src/Provers/simplifier.ML

   type solver
   val mk_solver: string -> (thm list -> int -> tactic) -> solver
   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,
     unsafe_solvers: solver list,
     solvers: solver list};

 
 (* type simpset *)
 
 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,
     unsafe_solvers: solver list,
     solvers: solver list};

       val solvs = app_sols (if safe then solvers else unsafe_solvers);
       fun simp_loop_tac i =
         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;
 
 val simp_tac = generic_simp_tac false (false, false, false);
 val asm_simp_tac = generic_simp_tac false (false, true, false);