# HG changeset patch # User wenzelm # Date 1011298020 -3600 # Node ID 787ecc2ac737ad09f7950e4048f967808e75d43c # Parent a529b4b918883eac4baf99e073fe70cf38ec3b3a RuleCases.make interface based on term instead of thm; diff -r a529b4b91888 -r 787ecc2ac737 src/Pure/Isar/rule_cases.ML --- 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;