1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Sep 25 20:04:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Sep 25 20:37:59 2015 +0200
     1.3 @@ -355,7 +355,7 @@
     1.4  fun print_intros ctxt gr consts =
     1.5    tracing (cat_lines (map (fn const =>
     1.6      "Constant " ^ const ^ "has intros:\n" ^
     1.7 -    cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
     1.8 +    cat_lines (map (Thm.string_of_thm ctxt) (Graph.get_node gr const))) consts))
     1.9  
    1.10  
    1.11  (* translation of moded predicates *)