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/Library/Old_SMT/old_z3_proof_reconstruction.ML
changeset 61268 abe08fb15a12
parent 60949 ccbf9379e355
child 64574 1134e4d5e5b7 
--- a/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -72,7 +72,7 @@
 fun pretty_goal ctxt thms t =
   [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
   |> not (null thms) ? cons (Pretty.big_list "assumptions:"
-       (map (Display.pretty_thm ctxt) thms))
+       (map (Thm.pretty_thm ctxt) thms))
 
 fun try_apply ctxt thms =
   let
isabelle