# HG changeset patch
# User wenzelm
# Date 1191882013 -7200
# Node ID 2a45e400fdad5c5916ed68a0b2bbeaea8a94d102
# Parent  ad3a8569759cc5cadf91342677a361989d1934e6
generic Syntax.pretty/string_of operations;

diff -r ad3a8569759c -r 2a45e400fdad NEWS
--- a/NEWS	Mon Oct 08 22:06:32 2007 +0200
+++ b/NEWS	Tue Oct 09 00:20:13 2007 +0200
@@ -1307,6 +1307,13 @@
 (Syntax.read_term etc.). These supersede former Sign.read_term etc.
 which are considered legacy and await removal.
 
+* Pure/Syntax: generic interfaces for type unchecking
+(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
+with common combinations (Syntax.pretty_term, Syntax.string_of_term
+etc.).  Former Sign.pretty_term, Sign.string_of_term etc. are still
+available for convenience, but refer to the very same operations
+(using a mere theory instead of a full context).
+
 * Isar: simplified treatment of user-level errors, using exception
 ERROR of string uniformly.  Function error now merely raises ERROR,
 without any side effect on output channels.  The Isar toplevel takes
diff -r ad3a8569759c -r 2a45e400fdad doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/doc-src/antiquote_setup.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -76,7 +76,7 @@
     #> space_implode "\\par\\smallskip%\n"
     #> enclose "\\isa{" "}");
 
-fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
 
 in
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -34,7 +34,7 @@
 fun print_structures ctxt =
   let
     val structs = Data.get (Context.Proof ctxt);
-    val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun pretty_struct ((s, ts), _) = Pretty.block
       [Pretty.str s, Pretty.str ":", Pretty.brk 1,
        Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Oct 09 00:20:13 2007 +0200
@@ -190,9 +190,9 @@
      of SOME t' => t'
       | NONE => evl thy t;
     val ty' = Term.type_of t';
-    val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
+    val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
       Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
-      Pretty.quote (ProofContext.pretty_typ ctxt ty')];
+      Pretty.quote (Syntax.pretty_typ ctxt ty')];
   in Pretty.writeln p end;
 
 val evaluate = gen_evaluate (map snd evaluators);
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -134,7 +134,7 @@
     inst >> Option.map (pair NONE);
 
 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
-  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t));
+  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Orderings.thy	Tue Oct 09 00:20:13 2007 +0200
@@ -275,9 +275,9 @@
   let
     val structs = Data.get (Context.Proof ctxt);
     fun pretty_term t = Pretty.block
-      [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1,
+      [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
         Pretty.str "::", Pretty.brk 1,
-        Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))];
+        Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
     fun pretty_struct ((s, ts), _) = Pretty.block
       [Pretty.str s, Pretty.str ":", Pretty.brk 1,
        Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/datatype_case.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -247,7 +247,7 @@
                 in (pat_rect1, tree)
                 end)
             | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
-                ProofContext.string_of_term ctxt t, i)
+                Syntax.string_of_term ctxt t, i)
           end
       | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
   in mk
@@ -260,13 +260,13 @@
   (fn x as Free (s, _) => (fn xs =>
         if member op aconv xs x then
           case_error (quote s ^ " occurs repeatedly in the pattern " ^
-            quote (ProofContext.string_of_term ctxt pat))
+            quote (Syntax.string_of_term ctxt pat))
         else x :: xs)
     | _ => I) pat [];
 
 fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
   let
-    fun string_of_clause (pat, rhs) = ProofContext.string_of_term ctxt
+    fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
       (Syntax.const "_case1" $ pat $ rhs);
     val _ = map (no_repeat_vars ctxt o fst) clauses;
     val rows = map_index (fn (i, (pat, rhs)) =>
@@ -333,8 +333,7 @@
             in
               (t' $ u', used'')
             end
-        | prep_pat t used = case_error ("Bad pattern: " ^
-            ProofContext.string_of_term ctxt t);
+        | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
       fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
             let val (l', cnstrts) = strip_constraints l
             in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -175,7 +175,7 @@
 
 fun split_def ctxt geq =
     let
-      fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
+      fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
       val (qs, imp) = open_all_all geq
 
       val gs = Logic.strip_imp_prems imp
@@ -214,7 +214,7 @@
                                 
       fun check geq = 
           let
-            fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
+            fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
                                   
             val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
                                  
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -25,7 +25,7 @@
     let 
       fun err str = error (cat_lines ["Malformed definition:",
                                       str ^ " not allowed in sequential mode.",
-                                      ProofContext.string_of_term ctxt geq])
+                                      Syntax.string_of_term ctxt geq])
       val thy = ProofContext.theory_of ctxt
                 
       fun check_constr_pattern (Bound _) = ()
@@ -235,7 +235,7 @@
 
 fun warn_if_redundant ctxt origs tss =
     let
-        fun msg t = "Ignoring redundant equation: " ^ quote (ProofContext.string_of_term ctxt t)
+        fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
                     
         val (tss', _) = chop (length origs) tss
         fun check ((_, t), []) = (Output.warning (msg t); [])
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -252,7 +252,7 @@
 
 fun no_order_msg ctxt table tl measure_funs =
     let
-      val prterm = ProofContext.string_of_term ctxt
+      val prterm = Syntax.string_of_term ctxt
       fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
 
       fun pr_goal t i =
@@ -292,7 +292,7 @@
       val clean_table = map (fn x => map (nth x) order) table
 
       val relation = mk_measures domT (map (nth measure_funs) order)
-      val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation))
+      val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
 
     in (* 4: proof reconstruction *)
       st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -247,11 +247,11 @@
 
 fun err_in_rule ctxt name t msg =
   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
-    ProofContext.string_of_term ctxt t, msg]);
+    Syntax.string_of_term ctxt t, msg]);
 
 fun err_in_prem ctxt name t p msg =
-  error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p,
-    "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]);
+  error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
+    "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
 
 val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
 
@@ -275,7 +275,7 @@
 
     fun check_ind err t = case dest_predicate cs params t of
         NONE => err (bad_app ^
-          commas (map (ProofContext.string_of_term ctxt) params))
+          commas (map (Syntax.string_of_term ctxt) params))
       | SOME (_, _, ys, _) =>
           if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
           then err bad_ind_occ else ();
@@ -431,7 +431,7 @@
 
     fun err msg =
       error (Pretty.string_of (Pretty.block
-        [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
+        [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
 
     val elims = Induct.find_casesP ctxt prop;
 
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -656,7 +656,7 @@
     (* implemented above, or 'is_split_thm' should be modified to filter it  *)
     (* out                                                                   *)
     | (t, ts) => (
-      warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^
+      warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
                " (with " ^ string_of_int (length ts) ^
                " argument(s)) not implemented; proof reconstruction is likely to fail");
       NONE
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -215,9 +215,9 @@
                        else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
                                    " but gets " ^ Int.toString (length tys) ^
                                    " type arguments\n" ^
-                                   space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^
+                                   space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
                                    " the terms are \n" ^
-                                   space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
+                                   space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
                        end
                 | NONE => (*Not a constant. Is it a type constructor?*)
               case Recon.strip_prefix ResClause.tconst_prefix a of
@@ -236,11 +236,11 @@
   fun fol_terms_to_hol ctxt fol_tms =
     let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
         val _ = Output.debug (fn () => "  calling type inference:")
-        val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
+        val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
         val ts' = infer_types ctxt ts;
         val _ = app (fn t => Output.debug
-                      (fn () => "  final term: " ^ ProofContext.string_of_term ctxt t ^
-                                "  of type  " ^ ProofContext.string_of_typ ctxt (type_of t)))
+                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
+                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
                     ts'
     in  ts'  end;
 
@@ -338,7 +338,7 @@
       else
         let
           val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
-          val _ = Output.debug (fn () => "  atom: " ^ ProofContext.string_of_term ctxt i_atm)
+          val _ = Output.debug (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
           val prems_th1 = prems_of i_th1
           val prems_th2 = prems_of i_th2
           val index_th1 = get_index (mk_not i_atm) prems_th1
@@ -373,10 +373,11 @@
                   val adjustment = get_ty_arg_size thy tm1
                   val p' = if adjustment > p then p else p-adjustment
                   val tm_p = List.nth(args,p')
-                    handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment  ^ " term " ^  ProofContext.string_of_term ctxt tm)
+                    handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
+                      Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
               in
                   Output.debug (fn () => "path_finder: " ^ Int.toString p ^
-                                        "  " ^ ProofContext.string_of_term ctxt tm_p);
+                                        "  " ^ Syntax.string_of_term ctxt tm_p);
                   if null ps   (*FIXME: why not use pattern-matching and avoid repetition*)
                   then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
                   else let val (r,t) = path_finder_FO tm_p ps
@@ -398,9 +399,9 @@
           | path_finder_lit tm_a idx = path_finder isFO tm_a idx
         val (tm_subst, body) = path_finder_lit i_atm fp
         val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
-        val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs)
-        val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm)
-        val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst)
+        val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+        val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+        val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
         val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
         val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
         val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -960,8 +960,7 @@
     val thy = ProofContext.theory_of ctxt;
   in
     Output.debug (fn () => "subgoals in isar_atp:\n" ^
-                  Pretty.string_of (ProofContext.pretty_term ctxt
-                    (Logic.mk_conjunction_list (Thm.prems_of goal))));
+                  Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
     Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
     app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
     if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -352,7 +352,7 @@
 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
   ATP may have their literals reordered.*)
 fun isar_lines ctxt ctms =
-  let val string_of = ProofContext.string_of_term ctxt
+  let val string_of = Syntax.string_of_term ctxt
       fun doline have (lname, t, []) =  (*No deps: it's a conjecture clause, with no proof.*)
            (case permuted_clause t ctms of
                 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
diff -r ad3a8569759c -r 2a45e400fdad src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -108,7 +108,7 @@
     val rhs_tfrees = Term.add_tfrees set [];
     val rhs_tfreesT = Term.add_tfreesT setT [];
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
-      error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
     fun mk_nonempty A =
       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
     val goal = mk_nonempty set;
@@ -232,7 +232,7 @@
 
 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
   let
-    val string_of_term = ProofContext.string_of_term (ProofContext.init thy);
+    val string_of_term = Sign.string_of_term thy;
     val name = the_default (#1 typ) opt_name;
     val (set, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
diff -r ad3a8569759c -r 2a45e400fdad src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -67,7 +67,7 @@
     val setT = Term.fastype_of set;
     val rhs_tfrees = term_tfrees set;
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
-      error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
     fun mk_nonempty A =
       HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
     fun mk_admissible A =
diff -r ad3a8569759c -r 2a45e400fdad src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -416,7 +416,7 @@
   (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
 
 fun trace_term ctxt msg t =
-  (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t)
+  (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
 
 fun trace_msg msg =
   if !trace then tracing msg else ();
@@ -562,7 +562,7 @@
   | (v, lineqs) :: hist' =>
       let
         val frees = map Free params
-        fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t))
+        fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
         val start =
           if v = ~1 then (hist', findex0 discr n lineqs)
           else (hist, replicate n Rat.zero)
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/args.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -170,8 +170,8 @@
   let
     val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
     fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s)
-      | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
-      | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
+      | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T
+      | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t
       | prt (Arg (_, Value (SOME (Fact ths)))) =
           Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
       | prt arg = Pretty.str (string_of arg);
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/class.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -413,6 +413,8 @@
 
 fun print_classes thy =
   let
+    val ctxt = ProofContext.init thy;
+
     val algebra = Sign.classes_of thy;
     val arities =
       Symtab.empty
@@ -423,13 +425,13 @@
     fun mk_arity class tyco =
       let
         val Ss = Sorts.mg_domain algebra tyco [class];
-      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
+      in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
     fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
-      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
+      ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
     fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
       (SOME o Pretty.str) ("class " ^ class ^ ":"),
       (SOME o Pretty.block) [Pretty.str "supersort: ",
-        (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
+        (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
       Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
       ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
         o these o Option.map #params o try (AxClass.get_definition thy)) class,
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/element.ML
--- 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 []))
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -40,9 +40,9 @@
     | Elim => Pretty.str (prfx "elim")
     | Dest => Pretty.str (prfx "dest")
     | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
-        Pretty.quote (ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat))]
+        Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
     | Pattern pat => Pretty.enclose (prfx " \"") "\""
-        [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
+        [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
   end;
 
 
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -562,7 +562,7 @@
   let
     val ctxt = Proof.context_of state;
     val prop = Syntax.read_prop ctxt s;
-  in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
+  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
 
 fun string_of_term state s =
   let
@@ -571,15 +571,15 @@
     val T = Term.type_of t;
   in
     Pretty.string_of
-      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
+      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
   end;
 
 fun string_of_type state s =
   let
     val ctxt = Proof.context_of state;
     val T = ProofContext.read_typ ctxt s;
-  in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
+  in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
   PrintMode.with_modes modes (fn () =>
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -472,7 +472,7 @@
 fun print_registrations show_wits loc ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
-    val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     val prt_thm = prt_term o prop_of;
     fun prt_inst ts =
         Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
@@ -1545,7 +1545,7 @@
 	| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
             handle Termtab.DUP t =>
 	      error ("Conflicting interpreting equations for term " ^
-		quote (ProofContext.string_of_term ctxt t))
+		quote (Syntax.string_of_term ctxt t))
   in ((id', eqns'), eqns') end;
 
 
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -71,7 +71,7 @@
       if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
     val _ = null bads orelse
       error ("Result contains obtained parameters: " ^
-        space_implode " " (map (ProofContext.string_of_term ctxt) bads));
+        space_implode " " (map (Syntax.string_of_term ctxt) bads));
   in tm end;
 
 fun eliminate fix_ctxt rule xs As thm =
@@ -217,8 +217,8 @@
     val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val cert = Thm.cterm_of thy;
-    val string_of_typ = ProofContext.string_of_typ ctxt;
-    val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
+    val string_of_typ = Syntax.string_of_typ ctxt;
+    val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
 
     fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
 
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -465,7 +465,7 @@
   let
     val thy = theory_of state;
     val ctxt = context_of state;
-    val string_of_term = ProofContext.string_of_term ctxt;
+    val string_of_term = Syntax.string_of_term ctxt;
     val string_of_thm = ProofContext.string_of_thm ctxt;
 
     val ngoals = Thm.nprems_of goal;
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -43,8 +43,8 @@
 
 fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
 
-val pprint_typ = pprint ProofContext.pretty_typ;
-val pprint_term = pprint ProofContext.pretty_term;
+val pprint_typ = pprint Syntax.pretty_typ;
+val pprint_term = pprint Syntax.pretty_term;
 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
 val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
@@ -136,7 +136,7 @@
 
 fun pretty_var ctxt (x, T) =
   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
-    Pretty.quote (ProofContext.pretty_typ ctxt T)];
+    Pretty.quote (Syntax.pretty_typ ctxt T)];
 
 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
 
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -273,10 +273,10 @@
       raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
-        with_context ProofContext.string_of_typ Ts @ with_context ProofContext.string_of_term ts)
+        with_context Syntax.string_of_typ Ts @ with_context Syntax.string_of_term ts)
   | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
   | exn_msg true (TERM (msg, ts)) =
-      raised "TERM" (msg :: with_context ProofContext.string_of_term ts)
+      raised "TERM" (msg :: with_context Syntax.string_of_term ts)
   | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   | exn_msg true (THM (msg, i, thms)) =
       raised ("THM " ^ string_of_int i) (msg :: with_context ProofContext.string_of_thm thms)
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Thy/term_style.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -55,14 +55,14 @@
       (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => (l, r)
-    | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
+    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
   end;
 
 fun style_parm_premise i ctxt t =
   let val prems = Logic.strip_imp_prems t in
     if i <= length prems then nth prems (i - 1)
     else error ("Not enough premises for prem" ^ string_of_int i ^
-      " in propositon: " ^ ProofContext.string_of_term ctxt t)
+      " in propositon: " ^ Syntax.string_of_term ctxt t)
   end;
 
 val _ = Context.add_setup
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -429,22 +429,23 @@
 
 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
 
-fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+
 fun pretty_term_abbrev ctxt =
   ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
 
 fun pretty_term_typ ctxt t =
-  ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
+  Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
 
-fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
+fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
 
 fun pretty_term_const ctxt t =
   if Term.is_Const t then pretty_term ctxt t
-  else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
+  else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
 
 fun pretty_abbrev ctxt t =
   let
-    fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
+    fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
     val (head, args) = Term.strip_comb t;
     val (c, T) = Term.dest_Const head handle TERM _ => err ();
     val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
@@ -519,7 +520,7 @@
   ("typeof", args Args.term (output pretty_term_typeof)),
   ("const", args Args.term (output pretty_term_const)),
   ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
-  ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
+  ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output (K pretty_text))),
   ("goals", output_goals true),
   ("subgoals", output_goals false),
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/axclass.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -148,7 +148,8 @@
 fun the_classrel thy (c1, c2) =
   (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
     SOME th => Thm.transfer thy th
-  | NONE => error ("Unproven class relation " ^ Sign.string_of_classrel thy [c1, c2]));
+  | NONE => error ("Unproven class relation " ^
+      Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
 
 fun put_classrel arg = map_instances (fn (classrel, arities) =>
   (insert (eq_fst op =) arg classrel, arities));
@@ -157,7 +158,8 @@
 fun the_arity thy a (c, Ss) =
   (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss)  of
     SOME th => Thm.transfer thy th
-  | NONE => error ("Unproven type arity " ^ Sign.string_of_arity thy (a, Ss, [c])));
+  | NONE => error ("Unproven type arity " ^
+      Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
 
 fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
   (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
@@ -173,7 +175,7 @@
     fun pretty_axclass (class, AxClass {def, intro, axioms, params}) =
       Pretty.block (Pretty.fbreaks
        [Pretty.block
-          [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
+          [Pretty.str "class ", Syntax.pretty_sort ctxt [class], Pretty.str ":"],
         Pretty.strs ("parameters:" :: params_of thy class),
         ProofContext.pretty_fact ctxt ("def", [def]),
         ProofContext.pretty_fact ctxt (introN, [intro]),
@@ -233,11 +235,12 @@
 
 fun prove_classrel raw_rel tac thy =
   let
+    val ctxt = ProofContext.init thy;
     val (c1, c2) = cert_classrel thy raw_rel;
-    val th = Goal.prove (ProofContext.init thy) [] []
+    val th = Goal.prove ctxt [] []
         (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
       cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
-        quote (Sign.string_of_classrel thy [c1, c2]));
+        quote (Syntax.string_of_classrel ctxt [c1, c2]));
   in
     thy
     |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
@@ -246,13 +249,14 @@
 
 fun prove_arity raw_arity tac thy =
   let
+    val ctxt = ProofContext.init thy;
     val arity = Sign.cert_arity thy raw_arity;
     val names = map (prefix arity_prefix) (Logic.name_arities arity);
     val props = Logic.mk_arities arity;
-    val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
+    val ths = Goal.prove_multi ctxt [] [] props
       (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
         cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
-          quote (Sign.string_of_arity thy arity));
+          quote (Syntax.string_of_arity ctxt arity));
   in
     thy
     |> PureThy.add_thms (map (rpair []) (names ~~ ths))
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/codegen.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -982,8 +982,7 @@
   | pretty_counterex ctxt (SOME cex) =
       Pretty.chunks (Pretty.str "Counterexample found:\n" ::
         map (fn (s, t) =>
-          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
-            ProofContext.pretty_term ctxt t]) cex);
+          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
 
 val auto_quickcheck = ref true;
 val auto_quickcheck_time_limit = ref 5000;
@@ -1043,8 +1042,8 @@
     val T = Term.type_of t;
   in
     Pretty.writeln
-      (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
+      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
   end);
 
 exception Evaluation of term;
diff -r ad3a8569759c -r 2a45e400fdad src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/display.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -146,12 +146,14 @@
 
 fun pretty_full_theory verbose thy =
   let
-    fun prt_cls c = Sign.pretty_sort thy [c];
-    fun prt_sort S = Sign.pretty_sort thy S;
-    fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
-    fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
+    val ctxt = ProofContext.init thy;
+
+    fun prt_cls c = Syntax.pretty_sort ctxt [c];
+    fun prt_sort S = Syntax.pretty_sort ctxt S;
+    fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+    fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
-    fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
+    fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify;
     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
     val prt_const' = Defs.pretty_const (Sign.pp thy);
diff -r ad3a8569759c -r 2a45e400fdad src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Tools/induct.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -718,7 +718,7 @@
     inst >> Option.map (pair NONE);
 
 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
-  error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
+  error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
 
 fun unless_more_args scan = Scan.unless (Scan.lift
   ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
diff -r ad3a8569759c -r 2a45e400fdad src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Tools/nbe.ML	Tue Oct 09 00:20:13 2007 +0200
@@ -393,8 +393,8 @@
     val t' = norm_term thy t;
     val ty' = Term.type_of t';
     val p = PrintMode.with_modes modes (fn () =>
-      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty')]) ();
+      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'), Pretty.fbrk,
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')]) ();
   in Pretty.writeln p end;