src/HOL/Tools/inductive_realizer.ML
changeset 32131 7913823f14e3
parent 32125 10e1a6ea8df9
parent 32091 30e2ffbba718
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Jul 22 10:49:26 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jul 22 11:23:09 2009 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    (case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
     1.5        [Thm.proof_of thm] [] of
     1.6      [name] => name
     1.7 -  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
     1.8 +  | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
     1.9  
    1.10  val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    1.11