# HG changeset patch
# User wenzelm
# Date 1257085485 -3600
# Node ID b1cf34f1855c066592a9d8fbd63250dadadddae0
# Parent  2912bf1871baf1f7c97fb1bbf7ebb46a377952de
modernized structure Rule_Cases;

diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -62,10 +62,10 @@
 
 in
 
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
 
 fun mk_case_names_exhausts descr new =
-  map (RuleCases.case_names o exhaust_cases descr o #1)
+  map (Rule_Cases.case_names o exhaust_cases descr o #1)
     (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
 
 end;
@@ -153,7 +153,7 @@
 
 fun projections rule =
   Project_Rule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
-  |> map (Drule.standard #> RuleCases.save rule);
+  |> map (Drule.standard #> Rule_Cases.save rule);
 
 val supp_prod = thm "supp_prod";
 val fresh_prod = thm "fresh_prod";
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -7,7 +7,7 @@
 sig
   val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
-    thm list -> int -> RuleCases.cases_tactic
+    thm list -> int -> Rule_Cases.cases_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 struct
@@ -31,9 +31,9 @@
 
 fun inst_mutual_rule ctxt insts avoiding rules =
   let
-    val (nconcls, joined_rule) = RuleCases.strict_mutual_rule ctxt rules;
+    val (nconcls, joined_rule) = Rule_Cases.strict_mutual_rule ctxt rules;
     val concls = Logic.dest_conjunctions (Thm.concl_of joined_rule);
-    val (cases, consumes) = RuleCases.get joined_rule;
+    val (cases, consumes) = Rule_Cases.get joined_rule;
 
     val l = length rules;
     val _ =
@@ -93,12 +93,12 @@
       split_all_tuples
       #> rename_params_rule true
         (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding);
-    fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
+    fun rule_cases r = Rule_Cases.make_nested true (Thm.prop_of r) (Induct.rulified_term r);
   in
     (fn i => fn st =>
       rules
       |> inst_mutual_rule ctxt insts avoiding
-      |> RuleCases.consume (flat defs) facts
+      |> Rule_Cases.consume (flat defs) facts
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -158,7 +158,7 @@
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
-    val induct_cases = map fst (fst (RuleCases.get (the
+    val induct_cases = map fst (fst (Rule_Cases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));
     val ([raw_induct'], ctxt') = Variable.import_terms false [prop_of raw_induct] ctxt;
     val concls = raw_induct' |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop |>
@@ -547,7 +547,7 @@
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
-        val ind_case_names = RuleCases.case_names induct_cases;
+        val ind_case_names = Rule_Cases.case_names induct_cases;
         val induct_cases' = Inductive.partition_rules' raw_induct
           (intrs ~~ induct_cases); 
         val thss' = map (map atomize_intr) thss;
@@ -558,9 +558,9 @@
           (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
         val strong_induct =
           if length names > 1 then
-            (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
+            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, RuleCases.consumes 1]);
+            [ind_case_names, Rule_Cases.consumes 1]);
         val ((_, [strong_induct']), ctxt') = LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_induct"),
             map (Attrib.internal o K) (#2 strong_induct)), [#1 strong_induct])
@@ -572,12 +572,12 @@
         LocalTheory.note Thm.generatedK
           ((rec_qualified (Binding.name "strong_inducts"),
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (RuleCases.consumes 1))]),
+             Attrib.internal (K (Rule_Cases.consumes 1))]),
            strong_inducts) |> snd |>
         LocalTheory.notes Thm.generatedK (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
-              [Attrib.internal (K (RuleCases.case_names (map snd cases))),
-               Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
+              [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
+               Attrib.internal (K (Rule_Cases.consumes 1))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -164,7 +164,7 @@
         [] => ()
       | xs => error ("Missing equivariance theorem for predicate(s): " ^
           commas_quote xs));
-    val induct_cases = map fst (fst (RuleCases.get (the
+    val induct_cases = map fst (fst (Rule_Cases.get (the
       (Induct.lookup_inductP ctxt (hd names)))));
     val induct_cases' = if null induct_cases then replicate (length intrs) ""
       else induct_cases;
@@ -449,7 +449,7 @@
       let
         val rec_name = space_implode "_" (map Long_Name.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
-        val ind_case_names = RuleCases.case_names induct_cases;
+        val ind_case_names = Rule_Cases.case_names induct_cases;
         val induct_cases' = Inductive.partition_rules' raw_induct
           (intrs ~~ induct_cases); 
         val thss' = map (map atomize_intr) thss;
@@ -458,9 +458,9 @@
           mk_ind_proof ctxt thss' |> Inductive.rulify;
         val strong_induct =
           if length names > 1 then
-            (strong_raw_induct, [ind_case_names, RuleCases.consumes 0])
+            (strong_raw_induct, [ind_case_names, Rule_Cases.consumes 0])
           else (strong_raw_induct RSN (2, rev_mp),
-            [ind_case_names, RuleCases.consumes 1]);
+            [ind_case_names, Rule_Cases.consumes 1]);
         val (induct_name, inducts_name) =
           case alt_name of
             NONE => (rec_qualified (Binding.name "strong_induct"),
@@ -477,7 +477,7 @@
         LocalTheory.note Thm.generatedK
           ((inducts_name,
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (RuleCases.consumes 1))]),
+             Attrib.internal (K (Rule_Cases.consumes 1))]),
            strong_inducts) |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -203,10 +203,10 @@
 
 in
 
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+fun mk_case_names_induct descr = Rule_Cases.case_names (induct_cases descr);
 
 fun mk_case_names_exhausts descr new =
-  map (RuleCases.case_names o exhaust_cases descr o #1)
+  map (Rule_Cases.case_names o exhaust_cases descr o #1)
     (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
 
 end;
@@ -328,7 +328,7 @@
       [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
        ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
     val unnamed_rules = map (fn induct =>
-      ((Binding.empty, [induct]), [RuleCases.inner_rule, Induct.induct_type ""]))
+      ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
         (Library.drop (length dt_names, inducts));
   in
     thy9
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -98,12 +98,12 @@
                  psimp_attribs psimps
             ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
             ||>> note_theorem ((qualify "pinduct",
-                   [Attrib.internal (K (RuleCases.case_names cnames)),
-                    Attrib.internal (K (RuleCases.consumes 1)),
+                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
+                    Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
             ||>> note_theorem ((qualify "termination", []), [termination])
             ||> (snd o note_theorem ((qualify "cases",
-                   [Attrib.internal (K (RuleCases.case_names cnames))]), [cases]))
+                   [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
 
           val cdata = FunctionCtxData { add_simps=addsmps, case_names=cnames, psimps=psimps',
@@ -153,7 +153,7 @@
             |> add_simps I "simps" simp_attribs tsimps |> snd
             |> note_theorem
                ((qualify "induct",
-                 [Attrib.internal (K (RuleCases.case_names case_names))]),
+                 [Attrib.internal (K (Rule_Cases.case_names case_names))]),
                 tinduct) |> snd
           end
     in
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -2332,7 +2332,7 @@
       in mk_casesrule lthy' pred nparams intros end  
     val cases_rules = map mk_cases preds
     val cases =
-      map (fn case_rule => RuleCases.Case {fixes = [],
+      map (fn case_rule => Rule_Cases.Case {fixes = [],
         assumes = [("", Logic.strip_imp_prems case_rule)],
         binds = [], cases = []}) cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -693,15 +693,15 @@
     val rec_name = Binding.name_of rec_binding;
     fun rec_qualified qualified = Binding.qualify qualified rec_name;
     val intr_names = map Binding.name_of intr_bindings;
-    val ind_case_names = RuleCases.case_names intr_names;
+    val ind_case_names = Rule_Cases.case_names intr_names;
     val induct =
       if coind then
-        (raw_induct, [RuleCases.case_names [rec_name],
-          RuleCases.case_conclusion (rec_name, intr_names),
-          RuleCases.consumes 1, Induct.coinduct_pred (hd cnames)])
+        (raw_induct, [Rule_Cases.case_names [rec_name],
+          Rule_Cases.case_conclusion (rec_name, intr_names),
+          Rule_Cases.consumes 1, Induct.coinduct_pred (hd cnames)])
       else if no_ind orelse length cnames > 1 then
-        (raw_induct, [ind_case_names, RuleCases.consumes 0])
-      else (raw_induct RSN (2, rev_mp), [ind_case_names, RuleCases.consumes 1]);
+        (raw_induct, [ind_case_names, Rule_Cases.consumes 0])
+      else (raw_induct RSN (2, rev_mp), [ind_case_names, Rule_Cases.consumes 1]);
 
     val (intrs', ctxt1) =
       ctxt |>
@@ -716,8 +716,8 @@
       LocalTheory.note kind ((rec_qualified true (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
         LocalTheory.note kind ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
-          [Attrib.internal (K (RuleCases.case_names cases)),
-           Attrib.internal (K (RuleCases.consumes 1)),
+          [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]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
@@ -732,7 +732,7 @@
         LocalTheory.notes kind [((rec_qualified true (Binding.name "inducts"), []),
           inducts |> map (fn (name, th) => ([th],
             [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (RuleCases.consumes 1)),
+             Attrib.internal (K (Rule_Cases.consumes 1)),
              Attrib.internal (K (Induct.induct_pred name))])))] |> snd
       end
   in (intrs', elims', induct', ctxt3) end;
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -343,7 +343,7 @@
     Simplifier.full_simplify (HOL_basic_ss addsimprocs
       [to_pred_simproc (mem_Collect_eq :: split_conv :: to_pred_simps)]) |>
     eta_contract_thm (is_pred pred_arities) |>
-    RuleCases.save thm
+    Rule_Cases.save thm
   end;
 
 val to_pred_att = Thm.rule_attribute o to_pred;
@@ -374,7 +374,7 @@
     Thm.instantiate ([], insts) |>
     Simplifier.full_simplify (HOL_basic_ss addsimps to_set_simps
         addsimprocs [strong_ind_simproc pred_arities, collect_mem_simproc]) |>
-    RuleCases.save thm
+    Rule_Cases.save thm
   end;
 
 val to_set_att = Thm.rule_attribute o to_set;
@@ -522,7 +522,7 @@
       Inductive.declare_rules kind rec_name coind no_ind cnames
       (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts
       (map (fn th => (to_set [] (Context.Proof ctxt3) th,
-         map fst (fst (RuleCases.get th)))) elims)
+         map fst (fst (Rule_Cases.get th)))) elims)
       raw_induct' ctxt3
   in
     ({intrs = intrs', elims = elims', induct = induct,
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -237,8 +237,8 @@
     val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns);
   in
     induct
-    |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
-    |> RuleCases.save induct
+    |> Rule_Cases.rename_params (map params_of (maps (map #1 o #3 o #2) descr))
+    |> Rule_Cases.save induct
   end;
 
 local
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/record.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -1553,7 +1553,7 @@
 
 (* attributes *)
 
-fun case_names_fields x = RuleCases.case_names ["fields"] x;
+fun case_names_fields x = Rule_Cases.case_names ["fields"] x;
 fun induct_type_global name = [case_names_fields, Induct.induct_type name];
 fun cases_type_global name = [case_names_fields, Induct.cases_type name];
 
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -118,7 +118,7 @@
     fst (fold_rev complete_split_rule_var vars (rl, xs))
     |> remove_internal_split
     |> Drule.standard
-    |> RuleCases.save rl
+    |> Rule_Cases.save rl
   end;
 
 
@@ -138,7 +138,7 @@
     |> fold_index one_goal xss
     |> Simplifier.full_simplify split_rule_ss
     |> Drule.standard
-    |> RuleCases.save rl
+    |> Rule_Cases.save rl
   end;
 
 
diff -r 2912bf1871ba -r b1cf34f1855c src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/HOL/Tools/typedef.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -152,13 +152,13 @@
                 ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
                 ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
                 ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
-                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
                 ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
-                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
                 ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
-                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
                 ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
-                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
+                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
             ||> Sign.parent_path;
           val info = {rep_type = oldT, abs_type = newT,
             Rep_name = full Rep_name, Abs_name = full Abs_name,
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -287,15 +287,15 @@
     "rename bound variables in abstractions" #>
   setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   setup (Binding.name "folded") folded "folded definitions" #>
-  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
+  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> Rule_Cases.consumes)
     "number of consumed facts" #>
-  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
+  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> Rule_Cases.case_names)
     "named rule cases" #>
   setup (Binding.name "case_conclusion")
-    (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
+    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
     "named conclusion of rule cases" #>
   setup (Binding.name "params")
-    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
+    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
     "named rule parameters" #>
   setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
     "result put into standard form (legacy)" #>
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -222,7 +222,7 @@
     val maxidx = fold (Term.maxidx_typ o snd o fst) vars ~1;
     val rule = Thm.incr_indexes (maxidx + 1) raw_rule;
 
-    val params = RuleCases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
+    val params = Rule_Cases.strip_params (Logic.nth_prem (1, Thm.prop_of rule));
     val m = length vars;
     val n = length params;
     val _ = m <= n orelse err "More variables than parameters in obtained rule" rule;
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -387,7 +387,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+  Rule_Cases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
 fun apply_method current_context meth state =
   let
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -112,9 +112,9 @@
   val add_assms_i: Assumption.export ->
     (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
-  val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
-  val get_case: Proof.context -> string -> string option list -> RuleCases.T
+  val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+  val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
+  val get_case: Proof.context -> string -> string option list -> Rule_Cases.T
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
@@ -169,7 +169,7 @@
     syntax: LocalSyntax.T,                            (*local syntax*)
     consts: Consts.T * Consts.T,                      (*local/global consts*)
     facts: Facts.T,                                   (*local facts*)
-    cases: (string * (RuleCases.T * bool)) list};     (*named case contexts*)
+    cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
 
 fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
   Ctxt {mode = mode, naming = naming, syntax = syntax,
@@ -1150,13 +1150,13 @@
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
-    val RuleCases.Case {fixes, assumes, binds, cases} = c;
+    val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
     val fixes' = replace fxs fixes;
     val binds' = map drop_schematic binds;
   in
     if null (fold (Term.add_tvarsT o snd) fixes []) andalso
       null (fold (fold Term.add_vars o snd) assumes []) then
-        RuleCases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
+        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
     else error ("Illegal schematic variable(s) in case " ^ quote name)
   end;
 
@@ -1172,9 +1172,9 @@
 
 fun case_result c ctxt =
   let
-    val RuleCases.Case {fixes, ...} = c;
+    val Rule_Cases.Case {fixes, ...} = c;
     val (ts, ctxt') = ctxt |> fold_map fix fixes;
-    val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
+    val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
   in
     ctxt'
     |> bind_terms (map drop_schematic binds)
@@ -1292,7 +1292,7 @@
 fun pretty_cases ctxt =
   let
     fun add_case (_, (_, false)) = I
-      | add_case (name, (c as RuleCases.Case {fixes, ...}, true)) =
+      | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
           cons (name, (fixes, case_result c ctxt));
     val cases = fold add_case (cases_of ctxt) [];
   in
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -47,7 +47,7 @@
   val strict_mutual_rule: Proof.context -> thm list -> int list * thm
 end;
 
-structure RuleCases: RULE_CASES =
+structure Rule_Cases: RULE_CASES =
 struct
 
 (** cases **)
@@ -379,5 +379,5 @@
 
 end;
 
-structure Basic_Rule_Cases: BASIC_RULE_CASES = RuleCases;
+structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
 open Basic_Rule_Cases;
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -177,7 +177,7 @@
         else
           T.assign (SOME (T.Term (the (AList.lookup (op =) term_insts xi)))) arg);
   in
-    Drule.instantiate insts thm |> RuleCases.save thm
+    Drule.instantiate insts thm |> Rule_Cases.save thm
   end;
 
 fun read_instantiate_mixed' ctxt (args, concl_args) thm =
diff -r 2912bf1871ba -r b1cf34f1855c src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -318,7 +318,7 @@
           end;
 
         val atts = map (Attrib.internal o K)
-          [RuleCases.consumes (~ (length obtains)), RuleCases.case_names case_names];
+          [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names];
         val prems = Assumption.local_prems_of elems_ctxt ctxt;
         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
diff -r 2912bf1871ba -r b1cf34f1855c src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/induct.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -216,8 +216,8 @@
 fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
 fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
 
-val consumes0 = RuleCases.consumes_default 0;
-val consumes1 = RuleCases.consumes_default 1;
+val consumes0 = Rule_Cases.consumes_default 0;
+val consumes1 = Rule_Cases.consumes_default 1;
 
 in
 
@@ -344,10 +344,10 @@
     val thy = ProofContext.theory_of ctxt;
 
     fun inst_rule r =
-      if null insts then `RuleCases.get r
+      if null insts then `Rule_Cases.get r
       else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
         |> maps (prep_inst ctxt align_left I)
-        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r);
+        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r);
 
     val ruleq =
       (case opt_rule of
@@ -359,9 +359,9 @@
   in
     fn i => fn st =>
       ruleq
-      |> Seq.maps (RuleCases.consume [] facts)
+      |> Seq.maps (Rule_Cases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
-        CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
+        CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule) cases)
           (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   end;
 
@@ -483,7 +483,7 @@
           in Logic.list_implies (map rename_asm As, C) end;
         val cp' = cterm_fun rename_prop (Thm.cprop_of thm);
         val thm' = Thm.equal_elim (Thm.reflexive cp') thm;
-      in [RuleCases.save thm thm'] end
+      in [Rule_Cases.save thm thm'] end
   | special_rename_params _ _ ths = ths;
 
 
@@ -570,7 +570,7 @@
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]
-  |> filter_out (forall RuleCases.is_inner_rule);
+  |> filter_out (forall Rule_Cases.is_inner_rule);
 
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
@@ -583,29 +583,29 @@
     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
 
     fun inst_rule (concls, r) =
-      (if null insts then `RuleCases.get r
+      (if null insts then `Rule_Cases.get r
        else (align_left "Rule has fewer conclusions than arguments given"
           (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
         |> maps (prep_inst ctxt align_right (atomize_term thy))
-        |> Drule.cterm_instantiate) r |> pair (RuleCases.get r))
+        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
       |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
 
     val ruleq =
       (case opt_rule of
-        SOME rs => Seq.single (inst_rule (RuleCases.strict_mutual_rule ctxt rs))
+        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
       | NONE =>
           (get_inductP ctxt facts @
             map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
-          |> map_filter (RuleCases.mutual_rule ctxt)
+          |> map_filter (Rule_Cases.mutual_rule ctxt)
           |> tap (trace_rules ctxt inductN o map #2)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
 
     fun rule_cases rule =
-      RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
+      Rule_Cases.make_nested false (Thm.prop_of rule) (rulified_term rule);
   in
     (fn i => fn st =>
       ruleq
-      |> Seq.maps (RuleCases.consume (flat defs) facts)
+      |> Seq.maps (Rule_Cases.consume (flat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
         (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
           (CONJUNCTS (ALLGOALS
@@ -643,7 +643,7 @@
 fun get_coinductP ctxt goal = find_coinductP ctxt (Logic.strip_assums_concl goal);
 
 fun main_prop_of th =
-  if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
+  if Rule_Cases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
 
 in
 
@@ -652,9 +652,9 @@
     val thy = ProofContext.theory_of ctxt;
 
     fun inst_rule r =
-      if null inst then `RuleCases.get r
+      if null inst then `Rule_Cases.get r
       else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
-        |> pair (RuleCases.get r);
+        |> pair (Rule_Cases.get r);
 
     fun ruleq goal =
       (case opt_rule of
@@ -666,12 +666,12 @@
   in
     SUBGOAL_CASES (fn (goal, i) => fn st =>
       ruleq goal
-      |> Seq.maps (RuleCases.consume [] facts)
+      |> Seq.maps (Rule_Cases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
-          CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
+          CASES (Rule_Cases.make_common false (thy, Thm.prop_of rule') cases)
             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   end;
 
diff -r 2912bf1871ba -r b1cf34f1855c src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/induct_tacs.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -86,9 +86,9 @@
     val argss = map (map (Option.map induct_var)) varss;
     val rule =
       (case opt_rules of
-        SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules)
+        SOME rules => #2 (Rule_Cases.strict_mutual_rule ctxt rules)
       | NONE =>
-          (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
+          (case map_filter (Rule_Cases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of
             (_, rule) :: _ => rule
           | [] => raise THM ("No induction rules", 0, [])));
 
diff -r 2912bf1871ba -r b1cf34f1855c src/Tools/project_rule.ML
--- a/src/Tools/project_rule.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/Tools/project_rule.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -47,8 +47,8 @@
         Thm.permute_prems 0 (~ k)
         #> singleton (Variable.export ctxt' ctxt)
         #> Drule.zero_var_indexes
-        #> RuleCases.save raw_rule
-        #> RuleCases.add_consumes k);
+        #> Rule_Cases.save raw_rule
+        #> Rule_Cases.add_consumes k);
   in map result is end;
 
 fun project ctxt i th = hd (projects ctxt [i] th);
diff -r 2912bf1871ba -r b1cf34f1855c src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Oct 30 18:33:21 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sun Nov 01 15:24:45 2009 +0100
@@ -66,7 +66,7 @@
 
   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
   val (intr_names, intr_tms) = split_list (map fst intr_specs);
-  val case_names = RuleCases.case_names intr_names;
+  val case_names = Rule_Cases.case_names intr_names;
 
   (*recT and rec_params should agree for all mutually recursive components*)
   val rec_hds = map head_of rec_tms;