RuleCases.make interface based on term instead of thm;

--- a/src/Pure/Isar/rule_cases.ML	Thu Jan 17 21:06:23 2002 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Jan 17 21:07:00 2002 +0100
@@ -17,7 +17,7 @@
   val add: thm -> thm * (string list * int)
   type T
   val empty: T
-  val make: bool -> thm -> string list -> (string * T) list
+  val make: bool -> Sign.sg * term -> string list -> (string * T) list
   val rename_params: string list list -> thm -> thm
   val params: string list list -> 'a attribute
 end;
@@ -90,20 +90,19 @@
 
 val empty = {fixes = [], assumes = [], binds = []};
 
-fun prep_case open_parms thm name i =
+fun prep_case open_parms sg prop name i =
   let
-    val (_, _, Bi, _) = Thm.dest_state (thm, i)
-      handle THM _ => raise THM ("More cases than premises in rule", 0, [thm]);
+    val Bi = Drule.norm_hhf sg (hd (#1 (Logic.strip_prems (i, [], Logic.skip_flexpairs prop))));
     val xs = map (if open_parms then I else apfst Syntax.internal) (Logic.strip_params Bi);
     val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi);
     val concl = Term.list_abs (xs, Logic.strip_assums_concl Bi);
-    val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment (Thm.sign_of_thm thm) concl));
+    val bind = ((case_conclN, 0), Some (ObjectLogic.drop_judgment sg concl));
   in (name, {fixes = xs, assumes = asms, binds = [bind]}) end;
 
-fun make open_parms raw_thm names =
-  let val thm = Tactic.norm_hhf raw_thm in
-    #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1))
-      (Library.drop (length names - Thm.nprems_of thm, names), ([], length names)))
+fun make open_parms (sg, prop) names =
+  let val nprems = Logic.count_prems (Logic.skip_flexpairs prop, 0) in
+    #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms sg prop name i :: cases, i - 1))
+      (Library.drop (length names - nprems, names), ([], length names)))
   end;