79 | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); |
79 | dest _ _ = raise TERM ("Expected " ^ string_of_int n ^ " binop arguments", [tm]); |
80 in cs ~~ dest n tm end; |
80 in cs ~~ dest n tm end; |
81 |
81 |
82 fun extract_fixes NONE prop = (strip_params prop, []) |
82 fun extract_fixes NONE prop = (strip_params prop, []) |
83 | extract_fixes (SOME outline) prop = |
83 | extract_fixes (SOME outline) prop = |
84 splitAt (length (Logic.strip_params outline), strip_params prop); |
84 chop (length (Logic.strip_params outline)) (strip_params prop); |
85 |
85 |
86 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], []) |
86 fun extract_assumes _ NONE prop = ([("", Logic.strip_assums_hyp prop)], []) |
87 | extract_assumes qual (SOME outline) prop = |
87 | extract_assumes qual (SOME outline) prop = |
88 let val (hyps, prems) = |
88 let val (hyps, prems) = |
89 splitAt (length (Logic.strip_assums_hyp outline), Logic.strip_assums_hyp prop) |
89 chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop) |
90 in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; |
90 in ([(qual case_hypsN, hyps)], [(qual case_premsN, prems)]) end; |
91 |
91 |
92 fun extract_case is_open thy (case_outline, raw_prop) name concls = |
92 fun extract_case is_open thy (case_outline, raw_prop) name concls = |
93 let |
93 let |
94 val rename = if is_open then I else (apfst Syntax.internal); |
94 val rename = if is_open then I else (apfst Syntax.internal); |