src/Pure/simplifier.ML

   fun extend ss = Raw_Simplifier.inherit_context empty_ss ss;
   val merge = merge_ss;
 );
 
 val get_ss = Simpset.get;
-fun map_ss f context = Simpset.map (with_context (Context.proof_of context) f) context;
+
+fun map_ss f context =
+  Simpset.map (Raw_Simplifier.with_context (Context.proof_of context) f) context;
 
 
 (* attributes *)
 
 fun attrib f = Thm.declaration_attribute (fn th => map_ss (fn ss => f (ss, [th])));

     val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs));
     val solve_tac = FIRST' (map (Raw_Simplifier.solver ss)
       (rev (if safe then solvers else unsafe_solvers)));
 
     fun simp_loop_tac i =
-      asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
+      Raw_Simplifier.asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN
       (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i));
   in simp_loop_tac end;
 
 local