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/Isar/element.ML
changeset 24920 2a45e400fdad
parent 24637 4d1876424529
child 25202 3a539d9995fb 
--- a/src/Pure/Isar/element.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/element.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -164,8 +164,8 @@
 
 fun pretty_stmt ctxt =
   let
-    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
-    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
+    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_terms = separate (Pretty.keyword "and") o map prt_term;
     val prt_name_atts = pretty_name_atts ctxt;
 
@@ -189,8 +189,8 @@
 
 fun pretty_ctxt ctxt =
   let
-    val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
-    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
+    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
     val prt_name_atts = pretty_name_atts ctxt;
 
@@ -310,7 +310,7 @@
         (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
 
 fun pretty_witness ctxt witn =
-  let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in
+  let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
     Pretty.block (prt_term (witness_prop witn) ::
       (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
          (map prt_term (witness_hyps witn))] else []))
isabelle