src/Pure/simplifier.ML

   include BASIC_SIMPLIFIER
   val map_simpset_global: (simpset -> simpset) -> theory -> theory
   val pretty_ss: Proof.context -> simpset -> Pretty.T
   val clear_ss: simpset -> simpset
   val debug_bounds: bool Unsynchronized.ref
+  val prems_of: simpset -> thm list
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
   val add_prems: thm list -> simpset -> simpset
   val inherit_context: simpset -> simpset -> simpset
   val the_context: simpset -> Proof.context

 
 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>
   let
     val trivialities = Drule.reflexive_thm :: trivs;
 
-    fun unsafe_solver_tac ss = FIRST' [resolve_tac (trivialities @ prems_of_ss ss), assume_tac];
+    fun unsafe_solver_tac ss =
+      FIRST' [resolve_tac (trivialities @ Raw_Simplifier.prems_of ss), assume_tac];
     val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
 
     (*no premature instantiation of variables during simplification*)
-    fun safe_solver_tac ss = FIRST' [match_tac (trivialities @ prems_of_ss ss), eq_assume_tac];
+    fun safe_solver_tac ss =
+      FIRST' [match_tac (trivialities @ Raw_Simplifier.prems_of ss), eq_assume_tac];
     val safe_solver = mk_solver "easy safe" safe_solver_tac;
 
     fun mk_eq thm =
       if can Logic.dest_equals (Thm.concl_of thm) then [thm]
       else [thm RS reflect] handle THM _ => [];