changeset 12311 | ce5f9e61c037 |
parent 12123 | 739eba13e2cd |
child 12381 | 5177845a34f5 |
--- a/src/Pure/Isar/induct_attrib.ML Wed Nov 28 00:44:37 2001 +0100 +++ b/src/Pure/Isar/induct_attrib.ML Wed Nov 28 00:46:26 2001 +0100 @@ -110,7 +110,6 @@ ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)), (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2))); val copy = I; - val finish = I; val prep_ext = I; fun merge (((casesT1, casesS1), (inductT1, inductS1)), ((casesT2, casesS2), (inductT2, inductS2))) =