Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
changeset 61268 abe08fb15a12
parent 59582 0fbed69ff081
child 62958 b41c1cb5e251 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -217,7 +217,7 @@
     val _ =
       if show_intermediate_results options then
         tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
-          commas (map (Display.string_of_thm_global thy) spec))
+          commas (map (Thm.string_of_thm_global thy) spec))
       else ()
   in
     spec
isabelle