# HG changeset patch
# User wenzelm
# Date 1257086666 -3600
# Node ID 470a7b233ee5022b51b8a263fb1638e7a7e6cd32
# Parent  b1cf34f1855c066592a9d8fbd63250dadadddae0
modernized structure Context_Rules;

diff -r b1cf34f1855c -r 470a7b233ee5 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/FOL/IFOL.thy	Sun Nov 01 15:44:26 2009 +0100
@@ -646,7 +646,7 @@
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
 
-setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
+setup {* Context_Rules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
 
 
 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
diff -r b1cf34f1855c -r 470a7b233ee5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/HOL.thy	Sun Nov 01 15:44:26 2009 +0100
@@ -853,7 +853,7 @@
       (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
 in
   Hypsubst.hypsubst_setup
-  #> ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
+  #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
 end
 *}
 
diff -r b1cf34f1855c -r 470a7b233ee5 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -159,11 +159,11 @@
     in
       lthy
       |> ProofContext.note_thmss ""
-         [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+         [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd
       |> ProofContext.note_thmss ""
-         [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+         [((Binding.empty, [Context_Rules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
       |> ProofContext.note_thmss ""
-         [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
+         [((Binding.name "termination", [Context_Rules.intro_bang (SOME 0)]),
            [([Goal.norm_result termination], [])])] |> snd
       |> Proof.theorem_i NONE afterqed [[(goal, [])]]
     end
diff -r b1cf34f1855c -r 470a7b233ee5 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -708,7 +708,7 @@
       LocalTheory.notes kind
         (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
           map (fn th => [([th],
-           [Attrib.internal (K (ContextRules.intro_query NONE)),
+           [Attrib.internal (K (Context_Rules.intro_query NONE)),
             Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
       map (hd o snd);
     val (((_, elims'), (_, [induct'])), ctxt2) =
@@ -719,7 +719,7 @@
           [Attrib.internal (K (Rule_Cases.case_names cases)),
            Attrib.internal (K (Rule_Cases.consumes 1)),
            Attrib.internal (K (Induct.cases_pred name)),
-           Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #>
+           Attrib.internal (K (Context_Rules.elim_query NONE))]), [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
       LocalTheory.note kind
         ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")),
diff -r b1cf34f1855c -r 470a7b233ee5 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Provers/blast.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -55,7 +55,7 @@
                  swrappers: (string * wrapper) list,
                  uwrappers: (string * wrapper) list,
                  safe0_netpair: netpair, safep_netpair: netpair,
-                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
+                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
   val cla_modifiers: Method.modifier parser list
   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
 end;
diff -r b1cf34f1855c -r 470a7b233ee5 src/Provers/clasimp.ML
--- 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
 
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
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -71,10 +71,11 @@
 
 val sym_add =
   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
-  #> ContextRules.elim_query NONE;
+  #> Context_Rules.elim_query NONE;
+
 val sym_del =
   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
-  #> ContextRules.rule_del;
+  #> Context_Rules.rule_del;
 
 
 (* symmetric *)
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -33,7 +33,7 @@
     attribute context_parser
 end;
 
-structure ContextRules: CONTEXT_RULES =
+structure Context_Rules: CONTEXT_RULES =
 struct
 
 
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -371,7 +371,7 @@
     in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
 
 val print_rules = Toplevel.unknown_context o
-  Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
+  Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of);
 
 val print_trans_rules = Toplevel.unknown_context o
   Toplevel.keep (Calculation.print_rules o Toplevel.context_of);
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -240,7 +240,7 @@
   let
     val rules =
       if not (null arg_rules) then arg_rules
-      else flat (ContextRules.find_rules false facts goal ctxt)
+      else flat (Context_Rules.find_rules false facts goal ctxt)
   in trace ctxt rules; tac rules facts i end);
 
 fun meth tac x = METHOD (HEADGOAL o tac x);
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -157,7 +157,7 @@
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
-      [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
+      [((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
     ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
diff -r b1cf34f1855c -r 470a7b233ee5 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -313,7 +313,7 @@
             ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
             ctxt' |> Variable.auto_fixes asm
             |> ProofContext.add_assms_i Assumption.assume_export
-              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
+              [((name, [Context_Rules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;
 
diff -r b1cf34f1855c -r 470a7b233ee5 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sun Nov 01 15:24:45 2009 +0100
+++ b/src/Tools/intuitionistic.ML	Sun Nov 01 15:44:26 2009 +0100
@@ -25,18 +25,18 @@
 
 fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
 
-val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
+val bires_tac = Tactic.biresolution_from_nets_tac Context_Rules.orderlist;
 
 fun safe_step_tac ctxt =
-  ContextRules.Swrap ctxt
+  Context_Rules.Swrap ctxt
    (eq_assume_tac ORELSE'
-    bires_tac true (ContextRules.netpair_bang ctxt));
+    bires_tac true (Context_Rules.netpair_bang ctxt));
 
 fun unsafe_step_tac ctxt =
-  ContextRules.wrap ctxt
+  Context_Rules.wrap ctxt
    (assume_tac APPEND'
-    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
-    bires_tac false (ContextRules.netpair ctxt));
+    bires_tac false (Context_Rules.netpair_bang ctxt) APPEND'
+    bires_tac false (Context_Rules.netpair ctxt));
 
 fun step_tac ctxt i =
   REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
@@ -75,13 +75,13 @@
     >> (pair (I: Proof.context -> Proof.context) o att);
 
 val modifiers =
- [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
-  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
-  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
-  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
-  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
-  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
-  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
+ [modifier destN Args.bang_colon Args.bang Context_Rules.dest_bang,
+  modifier destN Args.colon (Scan.succeed ()) Context_Rules.dest,
+  modifier elimN Args.bang_colon Args.bang Context_Rules.elim_bang,
+  modifier elimN Args.colon (Scan.succeed ()) Context_Rules.elim,
+  modifier introN Args.bang_colon Args.bang Context_Rules.intro_bang,
+  modifier introN Args.colon (Scan.succeed ()) Context_Rules.intro,
+  Args.del -- Args.colon >> K (I, Context_Rules.rule_del)];
 
 in