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/Modelcheck/ROOT.ML
ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
This is the ROOT file for the Eindhoven Modelchecker example
*)
use_thy"Example";