--- a/src/HOL/Tools/inductive_package.ML Fri May 16 23:25:37 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sat May 17 13:54:30 2008 +0200
@@ -180,7 +180,7 @@
[dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
(resolve_tac [le_funI, le_boolI'])) thm))]
| _ => [thm]
- end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm);
+ end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);