# HG changeset patch
# User wenzelm
# Date 1002201596 -7200
# Node ID 4f7ad093b413380fa8581430e29c71857b0812ba
# Parent  548ba68385a3e4cfbd13fb31df6134b8022b0ba0
qualify MetaSimplifier;

diff -r 548ba68385a3 -r 4f7ad093b413 TFL/rules.ML
--- a/TFL/rules.ML	Thu Oct 04 14:49:38 2001 +0200
+++ b/TFL/rules.ML	Thu Oct 04 15:19:56 2001 +0200
@@ -51,7 +51,7 @@
 (* For debugging my isabelle solver in the conditional rewriter *)
   val term_ref : term list ref
   val thm_ref : thm list ref
-  val mss_ref : meta_simpset list ref
+  val mss_ref : MetaSimplifier.meta_simpset list ref
   val tracing : bool ref
   val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
                              -> thm -> thm * term list
@@ -546,7 +546,7 @@
  * Trace information for the rewriter
  *---------------------------------------------------------------------------*)
 val term_ref = ref[] : term list ref
-val mss_ref = ref [] : meta_simpset list ref;
+val mss_ref = ref [] : MetaSimplifier.meta_simpset list ref;
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
 
@@ -674,7 +674,7 @@
      fun prover used mss thm =
      let fun cong_prover mss thm =
          let val dummy = say "cong_prover:"
-             val cntxt = prems_of_mss mss
+             val cntxt = MetaSimplifier.prems_of_mss mss
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (string_of_thm thm)
@@ -687,7 +687,7 @@
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
-                     val mss' = add_prems(mss, map ASSUME ants)
+                     val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants)
                      val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
                        handle U.ERR _ => Thm.reflexive lhs
                      val dummy = print_thms "proven:" [lhs_eq_lhs1]
@@ -709,7 +709,7 @@
                   val Q = get_lhs eq1
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
-                  val mss' = add_prems(mss, map ASSUME ants1)
+                  val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
                   val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
                                 handle U.ERR _ => Thm.reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
@@ -734,7 +734,7 @@
                  else
                  let val tych = cterm_of sign
                      val ants1 = map tych ants
-                     val mss' = add_prems(mss, map ASSUME ants1)
+                     val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
                      val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
                         (false,true,false) (prover used') mss' (tych Q)
                       handle U.ERR _ => Thm.reflexive (tych Q)
@@ -759,7 +759,7 @@
 
         fun restrict_prover mss thm =
           let val dummy = say "restrict_prover:"
-              val cntxt = rev(prems_of_mss mss)
+              val cntxt = rev(MetaSimplifier.prems_of_mss mss)
               val dummy = print_thms "cntxt:" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
@@ -806,7 +806,7 @@
     val ctm = cprop_of th
     val names = add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
-      (prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm
+      (prover names) (MetaSimplifier.add_congs(MetaSimplifier.mss_of [cut_lemma'], congs)) ctm
     val th2 = equal_elim th1 th
  in
  (th2, filter (not o restricted) (!tc_list))
diff -r 548ba68385a3 -r 4f7ad093b413 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Oct 04 14:49:38 2001 +0200
+++ b/src/Provers/simplifier.ML	Thu Oct 04 15:19:56 2001 +0200
@@ -21,7 +21,7 @@
   type simpset
   val empty_ss: simpset
   val rep_ss: simpset ->
-   {mss: meta_simpset,
+   {mss: MetaSimplifier.meta_simpset,
     mk_cong: thm -> thm,
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (int -> tactic)) list,
@@ -152,7 +152,7 @@
 
 datatype simpset =
   Simpset of {
-    mss: meta_simpset,
+    mss: MetaSimplifier.meta_simpset,
     mk_cong: thm -> thm,
     subgoal_tac: simpset -> int -> tactic,
     loop_tacs: (string * (int -> tactic)) list,
@@ -411,7 +411,7 @@
         asm_rewrite_goal_tac mode
           (solve_all_tac (mk_cong, subgoal_tac, loop_tacs, unsafe_solvers))
           mss i
-        THEN (solvs (prems_of_mss mss) i ORELSE
+        THEN (solvs (MetaSimplifier.prems_of_mss mss) i ORELSE
               TRY ((loop_tac loop_tacs THEN_ALL_NEW simp_loop_tac) i))
     in simp_loop_tac end;