src/HOL/Tools/inductive_realizer.ML
changeset 32091 30e2ffbba718
parent 31986 a68f88d264f7
child 32131 7913823f14e3
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 00:56:19 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jul 21 01:03:18 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