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/Sledgehammer/sledgehammer_isar_preplay.ML
changeset 61268 abe08fb15a12
parent 60549 e168d5c48a95
child 62219 dbac573b27e7 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -89,7 +89,7 @@
     val ctxt = ctxt |> Config.put show_markup true
     val assms = op @ assmsp
     val time = Pretty.str ("[" ^ string_of_play_outcome outcome ^ "]")
-    val assms = Pretty.enum " and " "using " " shows " (map (Display.pretty_thm ctxt) assms)
+    val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms)
     val concl = Syntax.pretty_term ctxt concl
   in
     tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl])))
isabelle