src/Provers/clasimp.ML
changeset 33369 470a7b233ee5
parent 32861 105f40051387
child 35613 9d3ff36ad4e1
--- a/src/Provers/clasimp.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/clasimp.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -139,9 +139,9 @@
 fun modifier att (x, ths) =
   fst (Library.foldl_map (Library.apply [att]) (x, rev ths));
 
-val addXIs = modifier (ContextRules.intro_query NONE);
-val addXEs = modifier (ContextRules.elim_query NONE);
-val delXs = modifier ContextRules.rule_del;
+val addXIs = modifier (Context_Rules.intro_query NONE);
+val addXEs = modifier (Context_Rules.elim_query NONE);
+val delXs = modifier Context_Rules.rule_del;
 
 in