changeset 33303 | 1e1210f31207 |
parent 32861 | 105f40051387 |
child 33368 | b1cf34f1855c |
--- a/src/Tools/induct.ML Thu Oct 29 12:59:25 2009 +0100 +++ b/src/Tools/induct.ML Thu Oct 29 13:21:38 2009 +0100 @@ -570,7 +570,7 @@ ((fn [] => NONE | ts => List.last ts) #> (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #> find_inductT ctxt)) [[]] - |> filter_out (forall Thm.is_internal); + |> filter_out (forall RuleCases.is_inner_rule); fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = [];