equal
deleted
inserted
replaced
44 |
44 |
45 val descr' = flat descr; |
45 val descr' = flat descr; |
46 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
46 val recTs = Datatype_Aux.get_rec_types descr' sorts; |
47 val newTs = take (length (hd descr)) recTs; |
47 val newTs = take (length (hd descr)) recTs; |
48 |
48 |
49 val {maxidx, ...} = rep_thm induct; |
49 val maxidx = Thm.maxidx_of induct; |
50 val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); |
50 val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct))); |
51 |
51 |
52 fun prove_casedist_thm (i, (T, t)) = |
52 fun prove_casedist_thm (i, (T, t)) = |
53 let |
53 let |
54 val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => |
54 val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) => |