src/HOL/Tools/inductive_package.ML
changeset 26928 ca87aff1ad2d
parent 26736 e6091328718f
child 26988 742e26213212
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri May 16 23:25:37 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat May 17 13:54:30 2008 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
     1.5           (resolve_tac [le_funI, le_boolI'])) thm))]
     1.6      | _ => [thm]
     1.7 -  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ string_of_thm thm);
     1.8 +  end handle THM _ => error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm thm);
     1.9  
    1.10  val mono_add = Thm.declaration_attribute (map_monos o fold Thm.add_thm o mk_mono);
    1.11  val mono_del = Thm.declaration_attribute (map_monos o fold Thm.del_thm o mk_mono);