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