changeset 61268 | abe08fb15a12 |
parent 59936 | b8ffc3dc9e24 |
child 61424 | c3658c18b7bc |
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:04:25 2015 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Sep 25 20:37:59 2015 +0200 @@ -355,7 +355,7 @@ fun print_intros ctxt gr consts = tracing (cat_lines (map (fn const => "Constant " ^ const ^ "has intros:\n" ^ - cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts)) + cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts)) (* translation of moded predicates *)