82 val xs = |
82 val xs = |
83 (rev (rename_wrt_term Bi (Logic.strip_params Bi))) (* FIXME avoid rename_wrt_term? *) |
83 (rev (rename_wrt_term Bi (Logic.strip_params Bi))) (* FIXME avoid rename_wrt_term? *) |
84 |> map (if open_parms then I else apfst Syntax.internal); |
84 |> map (if open_parms then I else apfst Syntax.internal); |
85 val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); |
85 val asms = map (curry Term.list_abs xs) (Logic.strip_assums_hyp Bi); |
86 val concl_bind = ((case_conclN, 0), |
86 val concl_bind = ((case_conclN, 0), |
87 Some (Term.list_abs (xs, AutoBind.drop_judgment (Logic.strip_assums_concl Bi)))); |
87 Some (Term.list_abs (xs, Logic.strip_assums_concl Bi))); |
88 in (name, {fixes = xs, assumes = asms, binds = [concl_bind]}) end; |
88 in (name, {fixes = xs, assumes = asms, binds = [concl_bind]}) end; |
89 |
89 |
90 fun make open_parms raw_thm names = |
90 fun make open_parms raw_thm names = |
91 let val thm = Tactic.norm_hhf raw_thm in |
91 let val thm = Tactic.norm_hhf raw_thm in |
92 #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1)) |
92 #1 (foldr (fn (name, (cases, i)) => (prep_case open_parms thm name i :: cases, i - 1)) |