--- a/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 25 20:37:59 2015 +0200
@@ -303,11 +303,11 @@
@{const_name Rings.divide}] a
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false))
| _ =>
(if Context_Position.is_visible ctxt then
- warning ("Lin. Arith.: wrong format for split rule " ^ Display.string_of_thm ctxt thm)
+ warning ("Lin. Arith.: wrong format for split rule " ^ Thm.string_of_thm ctxt thm)
else (); false));
(* substitute new for occurrences of old in a term, incrementing bound *)