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;