--- a/src/HOL/Decision_Procs/langford_data.ML Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Decision_Procs/langford_data.ML Thu Apr 18 17:07:01 2013 +0200
@@ -36,9 +36,11 @@
Thm.declaration_attribute (fn key => fn context => context |> Data.map
(del_data key #> apsnd (cons (key, entry))));
-val add_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.add_simp);
+val add_simp = Thm.declaration_attribute (fn th => fn context =>
+ (Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.add_simp th)) context);
-val del_simp = Thm.declaration_attribute (Data.map o apfst o Simplifier.del_simp);
+val del_simp = Thm.declaration_attribute (fn th => fn context =>
+ (Data.map o apfst) (simpset_map (Context.proof_of context) (Simplifier.del_simp th)) context);
fun match ctxt tm =
let