equal
deleted
inserted
replaced
34 let |
34 let |
35 val ty_str = case ty of |
35 val ty_str = case ty of |
36 Type(ty_str, _) => ty_str |
36 Type(ty_str, _) => ty_str |
37 | TFree(s,_) => error ("Free type: " ^ s) |
37 | TFree(s,_) => error ("Free type: " ^ s) |
38 | TVar((s,i),_) => error ("Free variable: " ^ s) |
38 | TVar((s,i),_) => error ("Free variable: " ^ s) |
39 val dt = Datatype.the_info thy ty_str |
39 val {induct, ...} = Datatype.the_info thy ty_str |
40 in |
40 in |
41 cases_thm_of_induct_thm (#induct dt) |
41 cases_thm_of_induct_thm induct |
42 end; |
42 end; |
43 |
43 |
44 |
44 |
45 (* for use when there are no prems to the subgoal *) |
45 (* for use when there are no prems to the subgoal *) |
46 (* does a case split on the given variable *) |
46 (* does a case split on the given variable *) |