changeset 59582 | 0fbed69ff081 |
parent 58826 | 2ed2eaabe3df |
child 59931 | 5ec4f97dd6d4 |
--- a/src/Tools/induction.ML Tue Mar 03 19:08:04 2015 +0100 +++ b/src/Tools/induction.ML Wed Mar 04 19:53:18 2015 +0100 @@ -20,7 +20,7 @@ if not(forall (null o #2 o #1) cases) then arg else let - val (prems, concl) = Logic.strip_horn (prop_of th); + val (prems, concl) = Logic.strip_horn (Thm.prop_of th); val prems' = drop consumes prems; val ps = preds_of concl;