diff -r cbc38731d42f -r 0fbed69ff081 src/Tools/induction.ML
--- 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;