equal
deleted
inserted
replaced
669 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
669 mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl' |
670 end |
670 end |
671 |
671 |
672 fun prove_strong_induct lthy induct exhausts size_thms bclausesss = |
672 fun prove_strong_induct lthy induct exhausts size_thms bclausesss = |
673 let |
673 let |
674 val ((insts, [induct']), lthy') = Variable.import true [induct] lthy |
674 val ((_, [induct']), lthy') = Variable.import true [induct] lthy |
675 |
675 |
676 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
676 val ([c_name, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
677 val c_ty = TFree (a, @{sort fs}) |
677 val c_ty = TFree (a, @{sort fs}) |
678 val c = Free (c_name, c_ty) |
678 val c = Free (c_name, c_ty) |
679 |
679 |