1.1 --- a/src/ZF/Tools/inductive_package.ML	Wed Jun 18 18:55:08 2008 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed Jun 18 18:55:10 2008 +0200
     1.3 @@ -277,7 +277,8 @@
     1.4        (Thm.assume A RS elim)
     1.5        |> Drule.standard';
     1.6    fun mk_cases a = make_cases (*delayed evaluation of body!*)
     1.7 -    (simpset ()) (Thm.read_cterm (Thm.theory_of_thm elim) (a, propT));
     1.8 +    (simpset ())
     1.9 +    let val thy = Thm.theory_of_thm elim in cterm_of thy (Syntax.read_prop_global thy a) end;
    1.10  
    1.11    fun induction_rules raw_induct thy =
    1.12     let