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/Pure/simplifier.ML
changeset 61268 abe08fb15a12
parent 61146 6fced6d926be
child 61841 4d3527b94f2a 
--- a/src/Pure/simplifier.ML	Fri Sep 25 20:04:25 2015 +0200
+++ b/src/Pure/simplifier.ML	Fri Sep 25 20:37:59 2015 +0200
@@ -162,8 +162,8 @@
 fun pretty_simpset verbose ctxt =
   let
     val pretty_term = Syntax.pretty_term ctxt;
-    val pretty_thm = Display.pretty_thm ctxt;
-    val pretty_thm_item = Display.pretty_thm_item ctxt;
+    val pretty_thm = Thm.pretty_thm ctxt;
+    val pretty_thm_item = Thm.pretty_thm_item ctxt;
 
     fun pretty_simproc (name, lhss) =
       Pretty.block
isabelle