# HG changeset patch
# User wenzelm
# Date 1449837860 -3600
# Node ID 2154e6c8d52dd33f434fff106da67c387b0d9eea
# Parent  4f5ab843cf5b573ebbf78ccdb8ad39c1a48a46f3
clarified modules;

diff -r 4f5ab843cf5b -r 2154e6c8d52d src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Fri Dec 11 13:44:20 2015 +0100
@@ -776,7 +776,7 @@
                 val goal' =
                   DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
                   |> Seq.maps (DETERM (do_retrofit ctxt'))
-                  |> Seq.map (fn goal => ([]: cases, goal));
+                  |> Seq.map (fn goal => ([]: Rule_Cases.cases, goal));
               in goal' end;
           in
             Seq.map apply_text texts
diff -r 4f5ab843cf5b -r 2154e6c8d52d src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Thu Dec 10 21:39:33 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Fri Dec 11 13:44:20 2015 +0100
@@ -7,7 +7,7 @@
 sig
   val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
-    thm list -> int -> Rule_Cases.cases_tactic
+    thm list -> int -> cases_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 struct
diff -r 4f5ab843cf5b -r 2154e6c8d52d src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Dec 10 21:39:33 2015 +0100
+++ b/src/Pure/Isar/method.ML	Fri Dec 11 13:44:20 2015 +0100
@@ -4,8 +4,21 @@
 Isar proof methods.
 *)
 
+infix 1 THEN_ALL_NEW_CASES;
+
+signature BASIC_METHOD =
+sig
+  type cases_state = Rule_Cases.cases * thm
+  type cases_tactic = thm -> cases_state Seq.seq
+  val CASES: Rule_Cases.cases -> tactic -> cases_tactic
+  val EMPTY_CASES: tactic -> cases_tactic
+  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
+  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
+end;
+
 signature METHOD =
 sig
+  include BASIC_METHOD
   type method = thm list -> cases_tactic
   val METHOD_CASES: (thm list -> cases_tactic) -> method
   val METHOD: (thm list -> tactic) -> method
@@ -92,7 +105,25 @@
 
 (** proof methods **)
 
-(* method *)
+(* tactics with cases *)
+
+type cases_state = Rule_Cases.cases * thm;
+type cases_tactic = thm -> cases_state Seq.seq;
+
+fun CASES cases tac st = Seq.map (pair cases) (tac st);
+fun EMPTY_CASES tac = CASES [] tac;
+
+fun SUBGOAL_CASES tac i st =
+  (case try Logic.nth_prem (i, Thm.prop_of st) of
+    SOME goal => tac (goal, i) st
+  | NONE => Seq.empty);
+
+fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
+  st |> tac1 i |> Seq.maps (fn (cases, st') =>
+    CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
+
+
+(* type method *)
 
 type method = thm list -> cases_tactic;
 
@@ -733,6 +764,9 @@
 
 end;
 
+structure Basic_Method: BASIC_METHOD = Method;
+open Basic_Method;
+
 val METHOD_CASES = Method.METHOD_CASES;
 val METHOD = Method.METHOD;
 val SIMPLE_METHOD = Method.SIMPLE_METHOD;
diff -r 4f5ab843cf5b -r 2154e6c8d52d src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Dec 10 21:39:33 2015 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Dec 11 13:44:20 2015 +0100
@@ -4,27 +4,14 @@
 Annotations and local contexts of rules.
 *)
 
-infix 1 THEN_ALL_NEW_CASES;
-
-signature BASIC_RULE_CASES =
-sig
-  type cases
-  type cases_state = cases * thm
-  type cases_tactic = thm -> cases_state Seq.seq
-  val CASES: cases -> tactic -> cases_tactic
-  val EMPTY_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
-  val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
-end
-
 signature RULE_CASES =
 sig
-  include BASIC_RULE_CASES
   datatype T = Case of
    {fixes: (binding * typ) list,
     assumes: (string * term list) list,
     binds: (indexname * term option) list,
     cases: (string * T) list}
+  type cases = (string * T option) list
   val case_hypsN: string
   val strip_params: term -> (string * typ) list
   type info = ((string * string list) * string list) list
@@ -184,25 +171,6 @@
 
 
 
-(** tactics with cases **)
-
-type cases_state = cases * thm;
-type cases_tactic = thm -> cases_state Seq.seq;
-
-fun CASES cases tac st = Seq.map (pair cases) (tac st);
-fun EMPTY_CASES tac = CASES [] tac;
-
-fun SUBGOAL_CASES tac i st =
-  (case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i) st
-  | NONE => Seq.empty);
-
-fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
-  st |> tac1 i |> Seq.maps (fn (cases, st') =>
-    CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
-
-
-
 (** annotations and operations on rules **)
 
 (* consume facts *)
@@ -483,6 +451,3 @@
   | SOME res => res);
 
 end;
-
-structure Basic_Rule_Cases: BASIC_RULE_CASES = Rule_Cases;
-open Basic_Rule_Cases;