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;