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/choice_specification.ML
changeset 61268 abe08fb15a12
parent 60825 bacfb7c45d81
child 67149 e61557884799 
--- a/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -148,7 +148,7 @@
             fun add_final (thm, thy) =
               if name = ""
               then (thm, thy)
-              else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
+              else (writeln ("  " ^ name ^ ": " ^ Thm.string_of_thm_global thy thm);
                 Global_Theory.store_thm (Binding.name name, thm) thy)
           in
             swap args
isabelle