# HG changeset patch
# User wenzelm
# Date 1292613695 -3600
# Node ID 42f24340ae53a5e08f86690547773e17431414ed
# Parent  4ae674714876fe682b3e7bae3ccf12c2e609fd78
more explicit references to structure Raw_Simplifier;

diff -r 4ae674714876 -r 42f24340ae53 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Dec 17 18:38:33 2010 +0100
+++ b/src/Pure/simplifier.ML	Fri Dec 17 20:21:35 2010 +0100
@@ -112,7 +112,9 @@
 );
 
 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 *)
@@ -231,7 +233,7 @@
       (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;