--- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 00:56:19 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 01:03:18 2009 +0200
@@ -19,7 +19,7 @@
(case Proofterm.fold_proof_atoms false (fn PThm (_, ((name, _, _), _)) => cons name | _ => I)
[Thm.proof_of thm] [] of
[name] => name
- | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm thm));
+ | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");