diff -r 847eefdca90d -r b01154b74314 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Jul 20 21:26:11 2016 +0200
+++ b/src/Pure/simplifier.ML	Wed Jul 20 22:36:10 2016 +0200
@@ -69,7 +69,10 @@
   val simp_modifiers': Method.modifier parser list
   val simp_modifiers: Method.modifier parser list
   val method_setup: Method.modifier parser list -> theory -> theory
-  val easy_setup: thm -> thm list -> theory -> theory
+  val unsafe_solver_tac: Proof.context -> int -> tactic
+  val unsafe_solver: solver
+  val safe_solver_tac: Proof.context -> int -> tactic
+  val safe_solver: solver
 end;
 
 structure Simplifier: SIMPLIFIER =
@@ -376,31 +379,22 @@
         (CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
     "simplification (all goals)";
 
-fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn ctxt0 =>
-  let
-    val trivialities = Drule.reflexive_thm :: trivs;
-
-    fun unsafe_solver_tac ctxt =
-      FIRST' [resolve_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
-    val unsafe_solver = mk_solver "easy unsafe" unsafe_solver_tac;
-
-    (*no premature instantiation of variables during simplification*)
-    fun safe_solver_tac ctxt =
-      FIRST' [match_tac ctxt (trivialities @ Raw_Simplifier.prems_of ctxt), eq_assume_tac];
-    val safe_solver = mk_solver "easy safe" safe_solver_tac;
+fun unsafe_solver_tac ctxt =
+  FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt];
+val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac;
 
-    fun mk_eq thm =
-      if can Logic.dest_equals (Thm.concl_of thm) then [thm]
-      else [thm RS reflect] handle THM _ => [];
+(*no premature instantiation of variables during simplification*)
+fun safe_solver_tac ctxt =
+  FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac];
+val safe_solver = mk_solver "Pure safe" safe_solver_tac;
 
-    fun mksimps thm = mk_eq (Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm);
-  in
-    empty_simpset ctxt0
-    setSSolver safe_solver
-    setSolver unsafe_solver
-    |> set_subgoaler asm_simp_tac
-    |> set_mksimps (K mksimps)
-  end));
+val _ =
+  Theory.setup
+    (method_setup [] #> Context.theory_map (map_ss (fn ctxt =>
+      empty_simpset ctxt
+      setSSolver safe_solver
+      setSolver unsafe_solver
+      |> set_subgoaler asm_simp_tac)));
 
 end;