changeset 12123 | 739eba13e2cd |
parent 12102 | a2deb1c3cd9b |
child 12311 | ce5f9e61c037 |
--- a/src/Pure/Isar/induct_attrib.ML Fri Nov 09 00:18:23 2001 +0100 +++ b/src/Pure/Isar/induct_attrib.ML Fri Nov 09 00:19:20 2001 +0100 @@ -110,6 +110,7 @@ ((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))) =