# HG changeset patch
# User wenzelm
# Date 1353180557 -3600
# Node ID 9e04e6edc5e768bfbd309666b632012e6e9241db
# Parent  c933c635843a92cc58103496be52de17ac330d8a
tuned;

diff -r c933c635843a -r 9e04e6edc5e7 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Nov 17 20:19:34 2012 +0100
+++ b/src/Provers/clasimp.ML	Sat Nov 17 20:29:17 2012 +0100
@@ -49,7 +49,7 @@
 
 (*Add a simpset to the claset!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
-val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" safe_asm_full_simp_tac;
+val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;
 
 
@@ -112,7 +112,7 @@
 (* tactics *)
 
 fun clarsimp_tac ctxt =
-  safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
+  Simplifier.safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
   Classical.clarify_tac (addSss ctxt);