/[mojave]/metaprl/refiner/reflib/theory.ml
ViewVC logotype

Diff of /metaprl/refiner/reflib/theory.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3583 by nogin, Fri Oct 22 01:07:59 1999 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 64  Line 64 
64  let record_theory thy =  let record_theory thy =
65     Ref_util.push thy base     Ref_util.push thy base
66    
67    let substitute_dforms orig upd =
68       let df = (List.find (fun b -> b.thy_name = upd) (!base)).thy_dformer in
69       let update b = if b.thy_name = orig then { b with thy_dformer = df } else b in
70          base := List.map update (!base)
71    
72  (*  (*
73   * Get all the theories.   * Get all the theories.
74   *)   *)

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26