src/HOL/Tools/inductive_set.ML
changeset 61268 abe08fb15a12
parent 61163 c94c65f35d01
child 61424 c3658c18b7bc
--- a/src/HOL/Tools/inductive_set.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -298,7 +298,7 @@
       val _ =
         if Context_Position.is_really_visible ctxt then
           warning ("Ignoring malformed set / predicate conversion rule: " ^ msg ^
-            "\n" ^ Display.string_of_thm ctxt thm)
+            "\n" ^ Thm.string_of_thm ctxt thm)
         else ();
     in tab end;