src/Tools/induct.ML

--- a/src/Tools/induct.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Tools/induct.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -573,7 +573,7 @@
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]
-  |> filter_out (forall PureThy.is_internal);
+  |> filter_out (forall Thm.is_internal);
 
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];