diff -r bdf01da93ed4 -r 69fe387b3b6e src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Jan 10 19:33:27 2006 +0100
+++ b/src/Provers/clasimp.ML	Tue Jan 10 19:33:29 2006 +0100
@@ -154,6 +154,14 @@
      delss (ss, [th]))
   end;
 
+fun modifier att (x, ths) =
+  fst (Thm.applys_attributes [att] (x, rev ths));
+
+fun addXIs which = modifier (which (ContextRules.intro_query NONE));
+fun addXEs which = modifier (which (ContextRules.elim_query NONE));
+fun addXDs which = modifier (which (ContextRules.dest_query NONE));
+fun delXs which = modifier (which ContextRules.rule_del);
+
 in
 
 val op addIffs =
@@ -168,21 +176,21 @@
 
 fun addIffs_global (thy, ths) =
   Library.foldl (addIff
-    (ContextRules.addXEs_global, ContextRules.addXIs_global)
-    (ContextRules.addXEs_global, ContextRules.addXIs_global) #1)
+    (addXEs Attrib.theory, addXIs Attrib.theory)
+    (addXEs Attrib.theory, addXIs Attrib.theory) #1)
   ((thy, ()), ths) |> #1;
 
 fun addIffs_local (ctxt, ths) =
   Library.foldl (addIff
-    (ContextRules.addXEs_local, ContextRules.addXIs_local)
-    (ContextRules.addXEs_local, ContextRules.addXIs_local) #1)
+    (addXEs Attrib.context, addXIs Attrib.context)
+    (addXEs Attrib.context, addXIs Attrib.context) #1)
   ((ctxt, ()), ths) |> #1;
 
 fun delIffs_global (thy, ths) =
-  Library.foldl (delIff ContextRules.delrules_global #1) ((thy, ()), ths) |> #1;
+  Library.foldl (delIff (delXs Attrib.theory) #1) ((thy, ()), ths) |> #1;
 
 fun delIffs_local (ctxt, ths) =
-  Library.foldl (delIff ContextRules.delrules_local #1) ((ctxt, ()), ths) |> #1;
+  Library.foldl (delIff (delXs Attrib.context) #1) ((ctxt, ()), ths) |> #1;
 
 end;