changeset 27865 | 27a8ad9612a3 |
parent 27809 | a1e409db516b |
child 28083 | 103d9282a946 |
--- 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 _ _ = [];