Now Datatype.occs_in_prems prints the necessary warning ITSELF.
It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).
(* Title: HOL/Nat.thy
ID: $Id$
Author: Tobias Nipkow
Copyright 1997 TU Muenchen
Nat is a partial order
*)
Nat = NatDef +
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
consts
"^" :: ['a::power,nat] => 'a (infixr 80)
end