diff -r b1cf34f1855c -r 470a7b233ee5 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/classical.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -45,7 +45,7 @@
                  uwrappers: (string * wrapper) list,
                  safe0_netpair: netpair, safep_netpair: netpair,
                  haz_netpair: netpair, dup_netpair: netpair,
-                 xtra_netpair: ContextRules.netpair}
+                 xtra_netpair: Context_Rules.netpair}
   val merge_cs          : claset * claset -> claset
   val addDs             : claset * thm list -> claset
   val addEs             : claset * thm list -> claset
@@ -224,7 +224,7 @@
          safep_netpair  : netpair,                 (*nets for >0 subgoals*)
          haz_netpair    : netpair,                 (*nets for unsafe rules*)
          dup_netpair    : netpair,                 (*nets for duplication*)
-         xtra_netpair   : ContextRules.netpair};   (*nets for extra rules*)
+         xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
 
 (*Desired invariants are
         safe0_netpair = build safe0_brls,
@@ -898,7 +898,7 @@
 fun haz_dest w = attrib (addE w o make_elim);
 val haz_elim = attrib o addE;
 val haz_intro = attrib o addI;
-val rule_del = attrib delrule o ContextRules.rule_del;
+val rule_del = attrib delrule o Context_Rules.rule_del;
 
 
 end;
@@ -914,11 +914,11 @@
 val setup_attrs =
   Attrib.setup @{binding swapped} (Scan.succeed swapped)
     "classical swap of introduction rule" #>
-  Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
+  Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query)
     "declaration of Classical destruction rule" #>
-  Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
+  Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query)
     "declaration of Classical elimination rule" #>
-  Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
+  Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query)
     "declaration of Classical introduction rule" #>
   Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
     "remove declaration of intro/elim/dest rule";
@@ -931,9 +931,9 @@
 
 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   let
-    val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
+    val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
     val CS {xtra_netpair, ...} = claset_of ctxt;
-    val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
+    val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
     val ruleq = Drule.multi_resolves facts rules;
   in