# HG changeset patch
# User wenzelm
# Date 1211115849 -7200
# Node ID 1035c89b4c02b79b956e761cbb6891686a8918fc
# Parent  64e850c3da9ed895296b79d2471f61f5989761bf
moved global pretty/string_of functions from Sign to Syntax;

diff -r 64e850c3da9e -r 1035c89b4c02 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/FOLP/simp.ML	Sun May 18 15:04:09 2008 +0200
@@ -381,12 +381,12 @@
 
 (*print lhs of conclusion of subgoal i*)
 fun pr_goal_lhs i st =
-    writeln (Sign.string_of_term (Thm.theory_of_thm st) 
+    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) 
              (lhs_of (prepare_goal i st)));
 
 (*print conclusion of subgoal i*)
 fun pr_goal_concl i st =
-    writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st)) 
+    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) 
 
 (*print subgoals i to j (inclusive)*)
 fun pr_goals (i,j) st =
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Complex/ex/linreif.ML	Sun May 18 15:04:09 2008 +0200
@@ -35,7 +35,7 @@
         | _ => error "num_of_term: unsupported Multiplication")
       | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
-      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
+      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
 
 (* pseudo reification : term -> fm *)
 fun fm_of_term vs t = 
@@ -56,7 +56,7 @@
 	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | Const("All",_)$Term.Abs(xn,xT,p) => 
 	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
-      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
+      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
 
 
 fun start_vs t =
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Complex/ex/linrtac.ML
--- a/src/HOL/Complex/ex/linrtac.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Complex/ex/linrtac.ML	Sun May 18 15:04:09 2008 +0200
@@ -91,7 +91,7 @@
     let val pth = linr_oracle thy (Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
-             Sign.string_of_term thy t1);
+             Syntax.string_of_term ctxt t1);
            ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
     end
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Complex/ex/mireif.ML
--- a/src/HOL/Complex/ex/mireif.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Complex/ex/mireif.ML	Sun May 18 15:04:09 2008 +0200
@@ -34,7 +34,7 @@
       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
       | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
-      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
+      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
         
 
 (* pseudo reification : term -> fm *)
@@ -58,7 +58,7 @@
         E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
       | Const("All",_)$Abs(xn,xT,p) => 
         A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
-      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
+      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
 
 fun start_vs t =
     let val fs = term_frees t
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Complex/ex/mirtac.ML
--- a/src/HOL/Complex/ex/mirtac.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Complex/ex/mirtac.ML	Sun May 18 15:04:09 2008 +0200
@@ -138,7 +138,7 @@
 	     else mirlfr_oracle sg (Pattern.eta_long [] t1)
     in 
           (trace_msg ("calling procedure with term:\n" ^
-             Sign.string_of_term sg t1);
+             Syntax.string_of_term ctxt t1);
            ((pth RS iffD2) RS pre_thm,
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
     end
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun May 18 15:04:09 2008 +0200
@@ -246,7 +246,7 @@
 
 fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
 fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
-fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
+fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
         (*val _ = writeln "Renaming:"
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Sun May 18 15:04:09 2008 +0200
@@ -48,11 +48,11 @@
           List.app (writeln o Context.str_of_thy) thys)
    | TERM (msg,ts) =>
          (writeln ("Exception TERM raised:\n" ^ msg);
-          List.app (writeln o Sign.string_of_term sign) ts)
+          List.app (writeln o Syntax.string_of_term_global sign) ts)
    | TYPE (msg,Ts,ts) =>
          (writeln ("Exception TYPE raised:\n" ^ msg);
-          List.app (writeln o Sign.string_of_typ sign) Ts;
-          List.app (writeln o Sign.string_of_term sign) ts)
+          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
+          List.app (writeln o Syntax.string_of_term_global sign) ts)
    | e => raise e
 
 (*Prints an exception, then fails*)
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Sun May 18 15:04:09 2008 +0200
@@ -51,7 +51,7 @@
   fun check_type T = 
     if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
     then T
-    else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses")
+    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
 
   fun dest_exs  0 t = t
     | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Library/comm_ring.ML	Sun May 18 15:04:09 2008 +0200
@@ -77,7 +77,7 @@
           val crhs = cterm_of thy (reif_polex T fs rhs);
           val ca = ctyp_of thy T;
         in (ca, cvs, clhs, crhs) end
-      else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
+      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
   | reif_eq _ _ = raise CRing "reif_eq: not an equation";
 
 (* The cring tactic *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Sun May 18 15:04:09 2008 +0200
@@ -33,7 +33,7 @@
 oracle mc_eindhoven_oracle ("term") =
 {*
 let
-  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term;
+  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
 
   fun call_mc s =
     let
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 15:04:09 2008 +0200
@@ -197,8 +197,8 @@
   | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
   | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
     let val thy = theory_of_thm t;
-	val fnam = Sign.string_of_term thy (getfun LHS);
-	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
+	val fnam = Syntax.string_of_term_global thy (getfun LHS);
+	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
 	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
     in
 	SOME (prove_goal thy gl (fn prems =>
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun May 18 15:04:09 2008 +0200
@@ -487,7 +487,7 @@
 fun string_of_terms sign terms =
 let fun make_string sign [] = "" |
  	make_string sign (trm::list) =
-           Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
+           Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
 in
   PrintMode.setmp ["Mucke"] (make_string sign) terms
 end;
@@ -689,7 +689,7 @@
  rc_in_term sg tl  _ l x 0 = rc_in_termlist sg tl l x |
  rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) |
  rc_in_term sg _ trm _ _ n =
- error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm));
+ error("malformed term for case-replacement: " ^ (Syntax.string_of_term_global sg trm));
  val (bv,n) = check_case sg tl (a $ b);
 in
  if (bv) then 
@@ -992,7 +992,7 @@
 fun analyze_types sg [] = [] |
 analyze_types sg [Type(a,[])] =
 (let
- val s = (Sign.string_of_typ sg (Type(a,[])))
+ val s = (Syntax.string_of_typ_global sg (Type(a,[])))
 in
  (if (s="bool") then ([]) else ([Type(a,[])]))
 end) |
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun May 18 15:04:09 2008 +0200
@@ -614,7 +614,7 @@
       let
         fun eqvt_err s = error
           ("Could not prove equivariance for introduction rule\n" ^
-           Sign.string_of_term (theory_of_thm intr)
+           Syntax.string_of_term_global (theory_of_thm intr)
              (Logic.unvarify (prop_of intr)) ^ "\n" ^ s);
         val res = SUBPROOF (fn {prems, params, ...} =>
           let
@@ -630,7 +630,7 @@
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
           NONE => eqvt_err ("Rule does not match goal\n" ^
-            Sign.string_of_term (theory_of_thm st) (hd (prems_of st)))
+            Syntax.string_of_term_global (theory_of_thm st) (hd (prems_of st)))
         | SOME (th, _) => Seq.single th
       end;
     val thss = map (fn atom =>
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sun May 18 15:04:09 2008 +0200
@@ -27,7 +27,7 @@
 
 fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
 fun primrec_eq_err thy s eq =
-  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
+  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
 
 
 (* preprocessing of equations *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Sun May 18 15:04:09 2008 +0200
@@ -501,7 +501,7 @@
      val dummy =
            if !trace then
                writeln ("ORIGINAL PROTO_DEF: " ^
-                          Sign.string_of_term thy proto_def)
+                          Syntax.string_of_term_global thy proto_def)
            else ()
      val R1 = S.rand WFR
      val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
@@ -541,7 +541,7 @@
      val R'abs = S.rand R'
      val proto_def' = subst_free[(R1,R')] proto_def
      val dummy = if !trace then writeln ("proto_def' = " ^
-                                         Sign.string_of_term
+                                         Syntax.string_of_term_global
                                          thy proto_def')
                            else ()
      val {lhs,rhs} = S.dest_eq proto_def'
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Sun May 18 15:04:09 2008 +0200
@@ -294,7 +294,7 @@
 fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
   let
     fun typ_error T msg = error ("Non-admissible type expression\n" ^
-      Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+      Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
 
     fun get_dt_descr T i tname dts =
       (case Symtab.lookup dt_info tname of
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -563,7 +563,7 @@
       Variable.importT_thms [induction] (Variable.thm_context induction);
 
     fun err t = error ("Ill-formed predicate in induction rule: " ^
-      Sign.string_of_term thy1 t);
+      Syntax.string_of_term_global thy1 t);
 
     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
           ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun May 18 15:04:09 2008 +0200
@@ -210,7 +210,7 @@
           end)
             (if is_set then [Mode (([], []), [], [])]
              else modes_of modes t handle Option =>
-               error ("Bad predicate: " ^ Sign.string_of_term thy t))
+               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
       | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
           else NONE) ps);
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Sun May 18 15:04:09 2008 +0200
@@ -166,9 +166,9 @@
     let val trands = terms_of rands
     in  if length trands = nargs then Term (list_comb(rator, trands))
         else error
-          ("apply_list: wrong number of arguments: " ^ Sign.string_of_term CPure.thy rator ^
-            " expected " ^
-            Int.toString nargs ^ " received " ^ commas (map (Sign.string_of_term CPure.thy) trands))
+          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global CPure.thy rator ^
+            " expected " ^ Int.toString nargs ^
+            " received " ^ commas (map (Syntax.string_of_term_global CPure.thy) trands))
     end;
 
 (*Instantiate constant c with the supplied types, but if they don't match its declared
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/old_primrec_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -27,7 +27,7 @@
 
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 fun primrec_eq_err thy s eq =
-  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
+  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
 
 
 (*the following code ensures that each recursive set always has the
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/refute.ML	Sun May 18 15:04:09 2008 +0200
@@ -219,7 +219,7 @@
     case get_first (fn (_, f) => f thy model args t)
       (#interpreters (RefuteData.get thy)) of
       NONE   => raise REFUTE ("interpret",
-        "no interpreter for term " ^ quote (Sign.string_of_term thy t))
+        "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t))
     | SOME x => x;
 
 (* ------------------------------------------------------------------------- *)
@@ -234,7 +234,7 @@
     case get_first (fn (_, f) => f thy model T intr assignment)
       (#printers (RefuteData.get thy)) of
       NONE   => raise REFUTE ("print",
-        "no printer for type " ^ quote (Sign.string_of_typ thy T))
+        "no printer for type " ^ quote (Syntax.string_of_typ_global thy T))
     | SOME x => x;
 
 (* ------------------------------------------------------------------------- *)
@@ -253,7 +253,7 @@
         "empty universe (no type variables in term)\n"
       else
         "Size of types: " ^ commas (map (fn (T, i) =>
-          Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
+          Syntax.string_of_typ_global thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
     val show_consts_msg =
       if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
         "set \"show_consts\" to show the interpretation of constants\n"
@@ -266,8 +266,8 @@
         cat_lines (List.mapPartial (fn (t, intr) =>
           (* print constants only if 'show_consts' is true *)
           if (!show_consts) orelse not (is_Const t) then
-            SOME (Sign.string_of_term thy t ^ ": " ^
-              Sign.string_of_term thy
+            SOME (Syntax.string_of_term_global thy t ^ ": " ^
+              Syntax.string_of_term_global thy
                 (print thy model (Term.type_of t) intr assignment))
           else
             NONE) terms) ^ "\n"
@@ -456,7 +456,7 @@
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",
             "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Sign.string_of_term CPure.thy t)
+            " in term " ^ Syntax.string_of_term_global CPure.thy t)
         | SOME typ =>
           typ)) t;
 
@@ -787,7 +787,7 @@
           TFree (_, sort) => sort
         | TVar (_, sort)  => sort
         | _               => raise REFUTE ("collect_axioms", "type " ^
-          Sign.string_of_typ thy T ^ " is not a variable"))
+          Syntax.string_of_typ_global thy T ^ " is not a variable"))
       (* obtain axioms for all superclasses *)
       val superclasses = sort @ (maps (Sign.super_classes thy) sort)
       (* merely an optimization, because 'collect_this_axiom' disallows *)
@@ -807,7 +807,7 @@
           (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
         | _ =>
           raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
-            Sign.string_of_term thy ax ^
+            Syntax.string_of_term_global thy ax ^
             ") contains more than one type variable")))
         class_axioms
     in
@@ -912,7 +912,7 @@
               val ax_in   = SOME (specialize_type thy (s, T) inclass)
                 (* type match may fail due to sort constraints *)
                 handle Type.TYPE_MATCH => NONE
-              val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax))
+              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
                 ax_in
               val ax_2 = Option.map (apsnd (specialize_type thy (s, T)))
                 (get_classdef thy class)
@@ -975,7 +975,7 @@
             val _ = if Library.exists (fn d =>
               case d of DatatypeAux.DtTFree _ => false | _ => true) typs then
               raise REFUTE ("ground_types", "datatype argument (for type "
-                ^ Sign.string_of_typ thy T ^ ") is not a variable")
+                ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
             else ()
             (* required for mutually recursive datatypes; those need to   *)
             (* be added even if they are an instance of an otherwise non- *)
@@ -1160,14 +1160,14 @@
     fun wrapper () =
     let
       val u      = unfold_defs thy t
-      val _      = writeln ("Unfolded term: " ^ Sign.string_of_term thy u)
+      val _      = writeln ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
       val axioms = collect_axioms thy u
       (* Term.typ list *)
       val types = Library.foldl (fn (acc, t') =>
         acc union (ground_types thy t')) ([], u :: axioms)
       val _     = writeln ("Ground types: "
         ^ (if null types then "none."
-           else commas (map (Sign.string_of_typ thy) types)))
+           else commas (map (Syntax.string_of_typ_global thy) types)))
       (* we can only consider fragments of recursive IDTs, so we issue a  *)
       (* warning if the formula contains a recursive IDT                  *)
       (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
@@ -1256,7 +1256,7 @@
       (* enter loop with or without time limit *)
       writeln ("Trying to find a model that "
         ^ (if negate then "refutes" else "satisfies") ^ ": "
-        ^ Sign.string_of_term thy t);
+        ^ Syntax.string_of_term_global thy t);
       if maxtime>0 then (
         TimeLimit.timeLimit (Time.fromSeconds maxtime)
           wrapper ()
@@ -2041,7 +2041,7 @@
                 then
                   raise REFUTE ("IDT_interpreter",
                     "datatype argument (for type "
-                    ^ Sign.string_of_typ thy (Type (s, Ts))
+                    ^ Syntax.string_of_typ_global thy (Type (s, Ts))
                     ^ ") is not a variable")
                 else ()
               (* if the model specifies a depth for the current type, *)
@@ -2165,7 +2165,7 @@
                 then
                   raise REFUTE ("IDT_constructor_interpreter",
                     "datatype argument (for type "
-                    ^ Sign.string_of_typ thy T
+                    ^ Syntax.string_of_typ_global thy T
                     ^ ") is not a variable")
                 else ()
               (* decrement depth for the IDT 'T' *)
@@ -2225,7 +2225,7 @@
                 then
                   raise REFUTE ("IDT_constructor_interpreter",
                     "datatype argument (for type "
-                    ^ Sign.string_of_typ thy (Type (s', Ts'))
+                    ^ Syntax.string_of_typ_global thy (Type (s', Ts'))
                     ^ ") is not a variable")
                 else ()
               (* split the constructors into those occuring before/after *)
@@ -3282,7 +3282,7 @@
               case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
             then
               raise REFUTE ("IDT_printer", "datatype argument (for type " ^
-                Sign.string_of_typ thy (Type (s, Ts)) ^ ") is not a variable")
+                Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable")
             else ()
           (* the index of the element in the datatype *)
           val element = (case intr of
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sun May 18 15:04:09 2008 +0200
@@ -79,7 +79,7 @@
                 val extraTs = rhs_extra_types (Ts ---> T) xtp
                 val _ = if null extraTs then () else
                    warning ("Skolemization: extra type vars: " ^
-                            commas_quote (map (Sign.string_of_typ thy) extraTs));
+                            commas_quote (map (Syntax.string_of_typ_global thy) extraTs));
                 val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
                 val args = argsx @ args0
                 val cT = extraTs ---> Ts ---> T
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Sun May 18 15:04:09 2008 +0200
@@ -164,8 +164,8 @@
 		fun resolution (c1, hyps1) (c2, hyps2) =
 		let
 			val _ = if !trace_sat then
-					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1))
-						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
+					tracing ("Resolving clause: " ^ Display.string_of_thm c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (#hyps (rep_thm c1))
+						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
 				else ()
 
 			(* the two literals used for resolution *)
@@ -191,7 +191,7 @@
 				(if hyp1_is_neg then c1' else c2')
 
 			val _ = if !trace_sat then
-					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
+					tracing ("Resulting clause: " ^ Display.string_of_thm c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (#hyps (rep_thm c_new)) ^ ")")
 				else ()
 			val _ = inc counter
 		in
@@ -390,7 +390,7 @@
 			val msg = "SAT solver found a countermodel:\n"
 				^ (commas
 					o map (fn (term, idx) =>
-						Sign.string_of_term (the_context ()) term ^ ": "
+						Syntax.string_of_term_global (the_context ()) term ^ ": "
 							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
 					(Termtab.dest atom_table)
 		in
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -147,9 +147,9 @@
                 case List.filter (fn t => let val (name,typ) = dest_Const t
                                      in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
                                      end) thawed_prop_consts of
-                    [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term thy c) ^ "\" found")
+                    [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
                   | [cf] => unvarify cf vmap
-                  | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term thy c) ^ "\" found (try applying explicit type constraints)")
+                  | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
             end
         val proc_consts = map proc_const consts
         fun mk_exist (c,prop) =
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -52,10 +52,10 @@
     val tab = TypecopyData.get thy;
     fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
       (Pretty.block o Pretty.breaks) [
-        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
+        Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
         Pretty.str "=",
         (Pretty.str o Sign.extern_const thy) constr,
-        Sign.pretty_typ thy typ,
+        Syntax.pretty_typ_global thy typ,
         Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
     in
       (Pretty.writeln o Pretty.block o Pretty.fbreaks)
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -223,8 +223,9 @@
     val name = the_default (#1 typ) opt_name;
     val (set, goal, _, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
-    val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
-      cat_error msg ("Failed to prove non-emptiness of " ^ quote (Sign.string_of_term thy set));
+    val non_empty = Goal.prove_global thy [] [] goal (K tac)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   in typedef_result non_empty thy end;
 
 in
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sun May 18 15:04:09 2008 +0200
@@ -239,7 +239,8 @@
 
  (*The oracle proves the given formula t, if possible*)
  fun oracle thy t =
-  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else ();
+  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
+   else ();
    if valid (expr_of false t) then t else fail t);
 
 end;
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOLCF/IOA/Modelcheck/MuIOA.thy
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sun May 18 15:04:09 2008 +0200
@@ -56,7 +56,7 @@
 end
 |
 IntC sg t =
-error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for IntC:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
 let
@@ -67,7 +67,7 @@
 end
 |
 StartC sg t =
-error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for StartC:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
 let
@@ -78,7 +78,7 @@
 end
 |
 TransC sg t =
-error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for TransC:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
 let
@@ -91,7 +91,7 @@
 end
 |
 IntA sg t =
-error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for IntA:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
 let
@@ -102,7 +102,7 @@
 end
 |
 StartA sg t =
-error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for StartA:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
 let
@@ -113,7 +113,7 @@
 end
 |
 TransA sg t =
-error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
+error("malformed automaton def for TransA:\n" ^ (Syntax.string_of_term_global sg t));
 
 fun delete_ul [] = []
 | delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
@@ -125,7 +125,7 @@
 fun delete_ul_string s = implode(delete_ul (explode s));
 
 fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
-type_list_of sign a = [(Sign.string_of_typ sign a)];
+type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
 
 fun structured_tuple l (Type("*",s::t::_)) =
 let
@@ -182,15 +182,15 @@
   let
     val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
     val concl = Logic.strip_imp_concl subgoal;
-    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
-    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
-	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
-	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
-	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
-	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
+    val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
+    val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));
+	val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));	
+	val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));
+	val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl));
+	val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl));
 	
 	val action_type_str =
-	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
+	Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
 
 	val abs_state_type_list =
 	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
@@ -291,7 +291,7 @@
 )
 end)
 handle malformed =>
-error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
+error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
 
 end
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -19,8 +19,8 @@
 structure IoaPackage: IOA_PACKAGE =
 struct
 
-val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ;
-val string_of_term = PrintMode.setmp [] o Sign.string_of_term;
+val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
 
 exception malformed;
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun May 18 15:04:09 2008 +0200
@@ -74,7 +74,7 @@
 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
 
 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
-fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
+fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
 
 (* ----- constructor list handling ----- *)
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -32,7 +32,7 @@
 
 fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
 fun fixrec_eq_err thy s eq =
-  fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
+  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
 
 (* ->> is taken from holcf_logic.ML *)
 (* TODO: fix dependencies so we can import HOLCFLogic here *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Provers/blast.ML	Sun May 18 15:04:09 2008 +0200
@@ -614,7 +614,7 @@
   | showTerm d (f $ u)       = if d=0 then dummyVar
                                else Term.$ (showTerm d f, showTerm (d-1) u);
 
-fun string_of thy d t = Sign.string_of_term thy (showTerm d t);
+fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
 
 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   Ex(P) is duplicated as the assumption ~Ex(P). *)
@@ -638,7 +638,7 @@
   in
       case topType thy t' of
           NONE   => stm   (*no type to attach*)
-        | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ thy T
+        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
   end;
 
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Isar/class.ML	Sun May 18 15:04:09 2008 +0200
@@ -722,7 +722,7 @@
     val inst_params = map_product get_param tycos params |> map_filter I;
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
-    val pp = Sign.pp thy;
+    val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy
       |> fold (fn tyco => Sorts.add_arities pp
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
@@ -793,7 +793,7 @@
     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
     fun pr_param ((c, _), (v, ty)) =
       (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
-        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
+        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   in
     (Pretty.block o Pretty.fbreaks)
       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML	Sun May 18 15:04:09 2008 +0200
@@ -62,7 +62,7 @@
   => (warning ("code generator: " ^ msg); NONE);
 fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
 
-fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
+fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
 fun string_of_const thy c = case AxClass.inst_of_param thy c
  of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
   | NONE => Sign.extern_const thy c;
@@ -269,7 +269,7 @@
 
 fun check_bare_const thy t = case try dest_Const t
  of SOME c_ty => c_ty
-  | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t);
+  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
 
 fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
   o check_bare_const thy;
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Isar/constdefs.ML	Sun May 18 15:04:09 2008 +0200
@@ -25,7 +25,7 @@
 fun gen_constdef prep_vars prep_prop prep_att
     structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
   let
-    fun err msg ts = error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
+    fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
     val thy_ctxt = ProofContext.init thy;
     val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun May 18 15:04:09 2008 +0200
@@ -174,7 +174,7 @@
     val overloading = get_overloading lthy;
     fun pr_operation ((c, ty), (v, _)) =
       (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
-        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Sign.pretty_typ thy ty];
+        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
   in
     (Pretty.block o Pretty.fbreaks)
       (Pretty.str "overloading" :: map pr_operation overloading)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun May 18 15:04:09 2008 +0200
@@ -284,7 +284,7 @@
 
 fun pretty_thm_legacy th =
   let val thy = Thm.theory_of_thm th
-  in Display.pretty_thm_aux (Syntax.pp (init thy)) true false [] th end;
+  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
 
 fun pretty_thm ctxt th =
   let val asms = map Thm.term_of (Assumption.assms_of ctxt)
@@ -365,7 +365,7 @@
   (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
    else Pretty.mark Markup.free (Pretty.str x))
   |> Pretty.mark
-    (if Variable.is_fixed ctxt x orelse Sign.is_pretty_global ctxt then Markup.fixed x
+    (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x
      else Markup.hilite);
 
 fun var_or_skolem _ s =
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun May 18 15:04:09 2008 +0200
@@ -278,7 +278,7 @@
   let
     val {typeof_eqns, ...} = ExtractionData.get thy;
     fun err () = error ("Unable to determine type of extracted program for\n" ^
-      Sign.string_of_term thy t)
+      Syntax.string_of_term_global thy t)
   in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
     [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
       Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
@@ -582,7 +582,7 @@
             | SOME rs => (case find vs' rs of
                 SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
               | NONE => error ("corr: no realizer for instance of theorem " ^
-                  quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
+                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Reconstruct.prop_of (proof_combt (prf0, ts))))))
           end
 
@@ -596,7 +596,7 @@
             else case find vs' (Symtab.lookup_list realizers s) of
               SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
             | NONE => error ("corr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end
 
@@ -691,7 +691,7 @@
             | SOME rs => (case find vs' rs of
                 SOME (t, _) => (defs, subst_TVars tye' t)
               | NONE => error ("extr: no realizer for instance of theorem " ^
-                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
+                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                     (Reconstruct.prop_of (proof_combt (prf0, ts))))))
           end
 
@@ -703,7 +703,7 @@
             case find vs' (Symtab.lookup_list realizers s) of
               SOME (t, _) => (defs, subst_TVars tye' t)
             | NONE => error ("extr: no realizer for instance of axiom " ^
-                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
+                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
                   (Reconstruct.prop_of (proof_combt (prf0, ts)))))
           end
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun May 18 15:04:09 2008 +0200
@@ -171,7 +171,7 @@
       | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
           (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
       | prf_of _ t = error ("Not a proof term:\n" ^
-          Sign.string_of_term thy t)
+          Syntax.string_of_term_global thy t)
 
   in prf_of [] end;
 
@@ -268,7 +268,7 @@
   in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
 
 fun pretty_proof thy prf =
-  Sign.pretty_term (proof_syntax prf thy) (term_of_proof prf);
+  Syntax.pretty_term_global (proof_syntax prf thy) (term_of_proof prf);
 
 fun pretty_proof_of full thm =
   pretty_proof (Thm.theory_of_thm thm) (proof_of full thm);
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Sun May 18 15:04:09 2008 +0200
@@ -51,8 +51,8 @@
             val {prop, ...} = rep_thm thm;
             val _ = if prop aconv prop' then () else
               error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
-                Sign.string_of_term thy prop ^ "\n\n" ^
-                Sign.string_of_term thy prop');
+                Syntax.string_of_term_global thy prop ^ "\n\n" ^
+                Syntax.string_of_term_global thy prop');
           in thm_of_atom thm Ts end
 
       | thm_of _ _ (PAxm (name, _, SOME Ts)) =
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Sun May 18 15:04:09 2008 +0200
@@ -65,7 +65,7 @@
     val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
   in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
   handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
-    Sign.string_of_typ thy T ^ "\n\n" ^ Sign.string_of_typ thy U);
+    Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
 
 fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
       (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
@@ -107,7 +107,7 @@
       handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
 
 fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
-  Sign.string_of_term thy t ^ "\n\n" ^ Sign.string_of_term thy u);
+  Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
 
 fun decompose thy Ts (env, p as (t, u)) =
   let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p
@@ -264,7 +264,7 @@
       let
         fun search env [] = error ("Unsolvable constraints:\n" ^
               Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
-                Display.pretty_flexpair (Sign.pp thy) (pairself
+                Display.pretty_flexpair (Syntax.pp_global thy) (pairself
                   (Envir.norm_term bigenv) p)) cs)))
           | search env ((u, p as (t1, t2), vs)::ps) =
               if u then
@@ -367,7 +367,7 @@
                 NONE =>
                   let
                     val _ = message ("Reconstructing proof of " ^ a);
-                    val _ = message (Sign.string_of_term thy prop);
+                    val _ = message (Syntax.string_of_term_global thy prop);
                     val prf' = forall_intr_vfs_prf prop
                       (reconstruct_proof thy prop cprf);
                     val (maxidx', prfs', prf) = expand
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun May 18 15:04:09 2008 +0200
@@ -698,7 +698,7 @@
         fun string_of_thm th = Output.output
                                (Pretty.string_of
                                    (Display.pretty_thm_aux
-                                        (Sign.pp (Thm.theory_of_thm th))
+                                        (Syntax.pp_global (Thm.theory_of_thm th))
                                         false (* quote *)
                                         false (* show hyps *)
                                         [] (* asms *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/axclass.ML	Sun May 18 15:04:09 2008 +0200
@@ -224,13 +224,14 @@
 
 fun cert_classrel thy raw_rel =
   let
+    val string_of_sort = Syntax.string_of_sort_global thy;
     val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
     val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy);
     val _ =
       (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
         [] => ()
-      | xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^
-          commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], []));
+      | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^
+          commas_quote xs ^ " of " ^ string_of_sort [c2], [], []));
   in (c1, c2) end;
 
 fun read_classrel thy raw_rel =
@@ -314,7 +315,7 @@
     val tyco = case inst_tyco_of thy (c, T)
      of SOME tyco => tyco
       | NONE => error ("Illegal type for instantiation of class parameter: "
-        ^ quote (c ^ " :: " ^ Sign.string_of_typ thy T));
+        ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
     val name_inst = instance_name (tyco, class) ^ "_inst";
     val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
     val T' = Type.strip_sorts T;
@@ -518,7 +519,8 @@
               | _ => I) typ [];
         val hyps = vars
           |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
-        val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
+        val ths = (typ, sort)
+          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
            {class_relation =
               fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
             type_constructor =
@@ -536,7 +538,7 @@
     val sort' = filter (is_none o lookup_type cache typ) sort;
     val ths' = derive_type thy (typ, sort')
       handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
-        Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort');
+        Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
     val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
     val ths =
       sort |> map (fn c =>
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/codegen.ML	Sun May 18 15:04:09 2008 +0200
@@ -582,13 +582,13 @@
 fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
    (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
       NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
-        Sign.string_of_term thy t)
+        Syntax.string_of_term_global thy t)
     | SOME x => x);
 
 fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
    (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
       NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
-        Sign.string_of_typ thy T)
+        Syntax.string_of_typ_global thy T)
     | SOME x => x);
 
 
@@ -987,10 +987,10 @@
         let val T = the_default (the_default (TFree p) default_type)
           (AList.lookup (op =) tvinsts s)
         in if Sign.of_sort thy (T, S) then T
-          else error ("Type " ^ Sign.string_of_typ thy T ^
+          else error ("Type " ^ Syntax.string_of_typ_global thy T ^
             " to be substituted for variable " ^
-            Sign.string_of_typ thy (TFree p) ^ "\ndoes not have sort " ^
-            Sign.string_of_sort thy S)
+            Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
+            Syntax.string_of_sort_global thy S)
         end))
       (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
   in test_term thy quiet size iterations gi' end;
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/display.ML
--- a/src/Pure/display.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/display.ML	Sun May 18 15:04:09 2008 +0200
@@ -86,7 +86,7 @@
   in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
 
 fun pretty_thm th =
-  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) true false [] th;
+  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
 
 val string_of_thm = Pretty.string_of o pretty_thm;
 
@@ -109,12 +109,12 @@
 
 (* other printing commands *)
 
-fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
 val print_ctyp = writeln o string_of_ctyp;
 
-fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
+fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
+fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
 val print_cterm = writeln o string_of_cterm;
 
 
@@ -138,7 +138,7 @@
     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);
+    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
@@ -326,7 +326,7 @@
   end;
 
 fun pretty_goals n th =
-  pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) Markup.none (true, true) n th;
+  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
 
 val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/drule.ML	Sun May 18 15:04:09 2008 +0200
@@ -826,12 +826,12 @@
         val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
         val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
           handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
-            Sign.string_of_typ thy' (Envir.norm_type tye T) ^
+            Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^
             "\nof variable " ^
-            Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^
+            Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^
             "\ncannot be unified with type\n" ^
-            Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^
-            Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u),
+            Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^
+            Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u),
             [T, U], [t, u])
     in  (thy', tye', maxi')  end;
 in
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/goal.ML	Sun May 18 15:04:09 2008 +0200
@@ -107,7 +107,7 @@
 fun prove_multi ctxt xs asms props tac =
   let
     val thy = ProofContext.theory_of ctxt;
-    val string_of_term = Sign.string_of_term thy;
+    val string_of_term = Syntax.string_of_term ctxt;
 
     fun err msg = cat_error msg
       ("The error(s) above occurred for the goal statement:\n" ^
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Sun May 18 15:04:09 2008 +0200
@@ -294,7 +294,7 @@
 in
 
 fun print_term ss warn a thy t = prnt ss warn (a ^ "\n" ^
-  Sign.string_of_term thy (if ! debug_simp then t else show_bounds ss t));
+  Syntax.string_of_term_global thy (if ! debug_simp then t else show_bounds ss t));
 
 fun debug warn a ss = if ! debug_simp then prnt ss warn (a ()) else ();
 fun trace warn a ss = if ! trace_simp then prnt ss warn (a ()) else ();
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/old_goals.ML	Sun May 18 15:04:09 2008 +0200
@@ -182,7 +182,7 @@
                 (string_of_int ngoals ^ " unsolved goals!")
             else if not (null hyps) then !result_error_fn state
                 ("Additional hypotheses:\n" ^
-                 cat_lines (map (Sign.string_of_term thy) hyps))
+                 cat_lines (map (Syntax.string_of_term_global thy) hyps))
             else if Pattern.matches thy
                                     (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
                  then final_th
@@ -207,11 +207,11 @@
           List.app (writeln o Context.str_of_thy) thys)
    | TERM (msg,ts) =>
          (writeln ("Exception TERM raised:\n" ^ msg);
-          List.app (writeln o Sign.string_of_term thy) ts)
+          List.app (writeln o Syntax.string_of_term_global thy) ts)
    | TYPE (msg,Ts,ts) =>
          (writeln ("Exception TYPE raised:\n" ^ msg);
-          List.app (writeln o Sign.string_of_typ thy) Ts;
-          List.app (writeln o Sign.string_of_term thy) ts)
+          List.app (writeln o Syntax.string_of_typ_global thy) Ts;
+          List.app (writeln o Syntax.string_of_term_global thy) ts)
    | e => raise e;
 
 (*Prints an exception, then fails*)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/pattern.ML	Sun May 18 15:04:09 2008 +0200
@@ -41,16 +41,17 @@
 
 val trace_unify_fail = ref false;
 
-fun string_of_term thy env binders t = Sign.string_of_term thy
-  (Envir.norm_term env (subst_bounds(map Free binders,t)));
+fun string_of_term thy env binders t =
+  Syntax.string_of_term_global thy
+    (Envir.norm_term env (subst_bounds (map Free binders, t)));
 
 fun bname binders i = fst (nth binders i);
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
 fun typ_clash thy (tye,T,U) =
   if !trace_unify_fail
-  then let val t = Sign.string_of_typ thy (Envir.norm_type tye T)
-           and u = Sign.string_of_typ thy (Envir.norm_type tye U)
+  then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
+           and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
        in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   else ()
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/sign.ML	Sun May 18 15:04:09 2008 +0200
@@ -61,16 +61,6 @@
   val intern_term: theory -> term -> term
   val extern_term: (string -> xstring) -> theory -> term -> term
   val intern_tycons: theory -> typ -> typ
-  val is_pretty_global: Proof.context -> bool
-  val set_pretty_global: bool -> Proof.context -> Proof.context
-  val init_pretty_global: theory -> Proof.context
-  val pretty_term: theory -> term -> Pretty.T
-  val pretty_typ: theory -> typ -> Pretty.T
-  val pretty_sort: theory -> sort -> Pretty.T
-  val string_of_term: theory -> term -> string
-  val string_of_typ: theory -> typ -> string
-  val string_of_sort: theory -> sort -> string
-  val pp: theory -> Pretty.pp
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
@@ -329,37 +319,12 @@
 
 
 
-(** pretty printing of terms, types etc. **)
-
-structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
-val is_pretty_global = PrettyGlobal.get;
-val set_pretty_global = PrettyGlobal.put;
-val init_pretty_global = set_pretty_global true o ProofContext.init;
-
-val pretty_term = Syntax.pretty_term o init_pretty_global;
-val pretty_typ = Syntax.pretty_typ o init_pretty_global;
-val pretty_sort = Syntax.pretty_sort o init_pretty_global;
-
-val string_of_term = Syntax.string_of_term o init_pretty_global;
-val string_of_typ = Syntax.string_of_typ o init_pretty_global;
-val string_of_sort = Syntax.string_of_sort o init_pretty_global;
-
-(*pp operations -- deferred evaluation*)
-fun pp thy = Pretty.pp
- (fn x => pretty_term thy x,
-  fn x => pretty_typ thy x,
-  fn x => pretty_sort thy x,
-  fn x => Syntax.pretty_classrel (init_pretty_global thy) x,
-  fn x => Syntax.pretty_arity (init_pretty_global thy) x);
-
-
-
 (** certify entities **)    (*exception TYPE*)
 
 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
 
 val certify_class         = Type.cert_class o tsig_of;
 val certify_sort          = Type.cert_sort o tsig_of;
@@ -416,10 +381,10 @@
     val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
-fun certify_term thy = certify' false (pp thy) true (consts_of thy) thy;
-fun certify_prop thy = certify' true (pp thy) true (consts_of thy) thy;
+fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
+fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
 
-fun cert_term_abbrev thy = #1 o certify' false (pp thy) false (consts_of thy) thy;
+fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
 val cert_prop = #1 oo certify_prop;
 
@@ -460,7 +425,7 @@
 
 fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
   let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
-  in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
+  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
 
 val read_arity = prep_arity intern_type Syntax.read_sort_global;
 val cert_arity = prep_arity (K I) certify_sort;
@@ -547,7 +512,7 @@
 
 fun read_def_terms (thy, types, sorts) used freeze sTs =
   let
-    val pp = pp thy;
+    val pp = Syntax.pp_global thy;
     val consts = consts_of thy;
     val cert_consts = Consts.certify pp (tsig_of thy) true consts;
     fun map_free x = if is_some (types (x, ~1)) then SOME x else NONE;
@@ -678,7 +643,7 @@
 
 fun add_abbrev mode tags (c, raw_t) thy =
   let
-    val pp = pp thy;
+    val pp = Syntax.pp_global thy;
     val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
@@ -706,12 +671,12 @@
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val syn' = Syntax.update_consts [bclass] syn;
-      val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
+      val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
     in (naming, syn', tsig', consts) end)
   |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
-fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (pp thy) arg);
-fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (pp thy) arg);
+fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
+fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
 
 
 (* add translation functions *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/tctical.ML	Sun May 18 15:04:09 2008 +0200
@@ -488,7 +488,7 @@
 
 fun print_vars_terms thy (n,thm) =
   let
-    fun typed ty = " has type: " ^ Sign.string_of_typ thy ty;
+    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
     fun find_vars thy (Const (c, ty)) =
         (case Term.typ_tvars ty
          of [] => I
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/theory.ML	Sun May 18 15:04:09 2008 +0200
@@ -162,7 +162,7 @@
 
 fun begin_theory name imports =
   let
-    val thy = Context.begin_thy Sign.pp name imports;
+    val thy = Context.begin_thy Syntax.pp_global name imports;
     val wrappers = begin_wrappers thy;
   in thy |> Sign.local_path |> apply_wrappers wrappers end;
 
@@ -185,7 +185,7 @@
         | TERM (msg, _) => error msg;
   in
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
-    (name, Sign.no_vars (Sign.pp thy) t)
+    (name, Sign.no_vars (Syntax.pp_global thy) t)
   end;
 
 fun read_axm thy (name, str) =
@@ -219,7 +219,7 @@
 
 fun dependencies thy unchecked is_def name lhs rhs =
   let
-    val pp = Sign.pp thy;
+    val pp = Syntax.pp_global thy;
     val consts = Sign.consts_of thy;
     fun prep const =
       let val Const (c, T) = Sign.no_vars pp (Const const)
@@ -256,7 +256,7 @@
 
     fun message txt =
       [Pretty.block [Pretty.str "Specification of constant ",
-        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)],
+        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
         Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   in
     if Sign.typ_instance thy (declT, T') then ()
@@ -281,7 +281,7 @@
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
-    Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
+    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
 
 
 (* add_defs(_i) *)
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/thm.ML	Sun May 18 15:04:09 2008 +0200
@@ -991,13 +991,13 @@
 
 local
 
-fun pretty_typing thy t T =
-  Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
+fun pretty_typing thy t T = Pretty.block
+  [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
 
 fun add_inst (ct, cu) (thy_ref, sorts) =
   let
-    val Cterm {t = t, T = T, ...} = ct
-    and Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
+    val Cterm {t = t, T = T, ...} = ct;
+    val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
     val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu);
     val sorts' = Sorts.union sorts_u sorts;
   in
@@ -1009,7 +1009,7 @@
         Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u])
     | _ => raise TYPE (Pretty.string_of (Pretty.block
        [Pretty.str "instantiate: not a variable",
-        Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t]))
+        Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t]))
   end;
 
 fun add_instT (cT, cU) (thy_ref, sorts) =
@@ -1021,10 +1021,10 @@
   in
     (case T of TVar (v as (_, S)) =>
       if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts'))
-      else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], [])
+      else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
     | _ => raise TYPE (Pretty.string_of (Pretty.block
         [Pretty.str "instantiate: not a type variable",
-         Pretty.fbrk, Sign.pretty_typ thy' T]), [T], []))
+         Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
   end;
 
 in
diff -r 64e850c3da9e -r 1035c89b4c02 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Pure/unify.ML	Sun May 18 15:04:09 2008 +0200
@@ -194,7 +194,7 @@
        handle Type.TUNIFY => raise CANTUNIFY;
 
 fun test_unify_types thy (args as (T,U,_)) =
-let val str_of = Sign.string_of_typ thy;
+let val str_of = Syntax.string_of_typ_global thy;
     fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
     val env' = unify_types thy args
 in if is_TVar(T) orelse is_TVar(U) then warn() else ();
@@ -556,7 +556,7 @@
     t is always flexible.*)
 fun print_dpairs thy msg (env,dpairs) =
   let fun pdp (rbinder,t,u) =
-        let fun termT t = Sign.pretty_term thy
+        let fun termT t = Syntax.pretty_term_global thy
                               (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
             val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
                           termT t];
diff -r 64e850c3da9e -r 1035c89b4c02 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Sun May 18 15:04:09 2008 +0200
@@ -73,7 +73,7 @@
       | mk_inst ty (TFree (_, sort)) = cons (ty, sort)
       | mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2;
     fun of_sort_deriv (ty, sort) =
-      Sorts.of_sort_derivation (Sign.pp thy) algebra
+      Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
         { class_relation = class_relation, type_constructor = type_constructor,
           type_variable = type_variable }
         (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
@@ -108,7 +108,7 @@
   | resort_thms algebra tap_typ (thms as thm :: _) =
       let
         val thy = Thm.theory_of_thm thm;
-        val pp = Sign.pp thy;
+        val pp = Syntax.pp_global thy;
         val cs = fold_consts (insert (op =)) thms [];
         fun match_const c (ty, ty_decl) =
           let
@@ -279,7 +279,7 @@
 fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
   let
     val ct = cterm_of proto_ct;
-    val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
+    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
     val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
     fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
       t [];
diff -r 64e850c3da9e -r 1035c89b4c02 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Tools/code/code_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -125,7 +125,7 @@
 fun eval evaluate term_of reff thy ct args =
   let
     val _ = if null (term_frees (term_of ct)) then () else error ("Term "
-      ^ quote (Sign.string_of_term thy (term_of ct))
+      ^ quote (Syntax.string_of_term_global thy (term_of ct))
       ^ " to be evaluated contains free variables");
   in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end;
 
diff -r 64e850c3da9e -r 1035c89b4c02 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/Tools/code/code_thingol.ML	Sun May 18 15:04:09 2008 +0200
@@ -430,7 +430,7 @@
       #>> (fn (tyco, tys) => tyco `%% tys)
 and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
   let
-    val pp = Sign.pp thy;
+    val pp = Syntax.pp_global thy;
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));
diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Datatype_ZF.thy	Sun May 18 15:04:09 2008 +0200
@@ -97,7 +97,7 @@
          (fn _ => rtac iff_reflection 1 THEN
            simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
          handle ERROR msg =>
-         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
+         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
           raise Match)
    in SOME thm end
    handle Match => NONE;
diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -54,7 +54,7 @@
     let val rec_hds = map head_of rec_tms
         val dummy = assert_all is_Const rec_hds
           (fn t => "Datatype set not previously declared as constant: " ^
-                   Sign.string_of_term @{theory IFOL} t);
+                   Syntax.string_of_term_global @{theory IFOL} t);
         val rec_names = (*nat doesn't have to be added*)
 	    @{const_name nat} :: map (#1 o dest_Const) rec_hds
 	val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
@@ -72,7 +72,7 @@
 
   val dummy = assert_all is_Const rec_hds
           (fn t => "Datatype set not previously declared as constant: " ^
-                   Sign.string_of_term thy t);
+                   Syntax.string_of_term_global thy t);
 
   val rec_names = map (#1 o dest_Const) rec_hds
   val rec_base_names = map Sign.base_name rec_names
diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sun May 18 15:04:09 2008 +0200
@@ -120,7 +120,7 @@
     (*analyze the LHS of a case equation to get a constructor*)
     fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
       | const_of eqn = error ("Ill-formed case equation: " ^
-                              Sign.string_of_term thy eqn);
+                              Syntax.string_of_term_global thy eqn);
 
     val constructors =
         map (head_of o const_of o FOLogic.dest_Trueprop o
diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Sun May 18 15:04:09 2008 +0200
@@ -24,7 +24,7 @@
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 
 fun primrec_eq_err sign s eq =
-  primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
+  primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq);
 
 
 (* preprocessing of equations *)
@@ -125,8 +125,8 @@
       in
           if !Ind_Syntax.trace then
               writeln ("recursor_rhs = " ^
-                       Sign.string_of_term thy recursor_rhs ^
-                       "\nabs = " ^ Sign.string_of_term thy abs)
+                       Syntax.string_of_term_global thy recursor_rhs ^
+                       "\nabs = " ^ Syntax.string_of_term_global thy abs)
           else();
           if Logic.occs (fconst, abs) then
               primrec_eq_err thy
@@ -152,7 +152,7 @@
   in
       if !Ind_Syntax.trace then
             writeln ("primrec def:\n" ^
-                     Sign.string_of_term thy def_tm)
+                     Syntax.string_of_term_global thy def_tm)
       else();
       (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
        def_tm)
diff -r 64e850c3da9e -r 1035c89b4c02 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat May 17 23:53:20 2008 +0200
+++ b/src/ZF/ind_syntax.ML	Sun May 18 15:04:09 2008 +0200
@@ -13,7 +13,7 @@
 val trace = ref false;
 
 fun traceIt msg thy t =
-  if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
+  if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
   else t;
 
 
@@ -46,7 +46,7 @@
 (*As above, but return error message if bad*)
 fun rule_concl_msg sign rl = rule_concl rl
     handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
-                          Sign.string_of_term sign rl);
+                          Syntax.string_of_term_global sign rl);
 
 (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   read_instantiate replaces a propositional variable by a formula variable*)