moved global pretty/string_of functions from Sign to Syntax;
authorwenzelm
Sun May 18 15:04:09 2008 +0200 (2008-05-18)
changeset 269391035c89b4c02
parent 26938 64e850c3da9e
child 26940 80df961f7900
moved global pretty/string_of functions from Sign to Syntax;
src/FOLP/simp.ML
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/linrtac.ML
src/HOL/Complex/ex/mireif.ML
src/HOL/Complex/ex/mirtac.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/comm_ring.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/old_primrec_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typecopy_package.ML
src/HOL/Tools/typedef_package.ML
src/HOL/ex/svc_funcs.ML
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/fixrec_package.ML
src/Provers/blast.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code_unit.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/proofchecker.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/meta_simplifier.ML
src/Pure/old_goals.ML
src/Pure/pattern.ML
src/Pure/sign.ML
src/Pure/tctical.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_package.ML
src/Tools/code/code_thingol.ML
src/ZF/Datatype_ZF.thy
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/primrec_package.ML
src/ZF/ind_syntax.ML
     1.1 --- a/src/FOLP/simp.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -381,12 +381,12 @@
     1.4  
     1.5  (*print lhs of conclusion of subgoal i*)
     1.6  fun pr_goal_lhs i st =
     1.7 -    writeln (Sign.string_of_term (Thm.theory_of_thm st) 
     1.8 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) 
     1.9               (lhs_of (prepare_goal i st)));
    1.10  
    1.11  (*print conclusion of subgoal i*)
    1.12  fun pr_goal_concl i st =
    1.13 -    writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st)) 
    1.14 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) 
    1.15  
    1.16  (*print subgoals i to j (inclusive)*)
    1.17  fun pr_goals (i,j) st =
     2.1 --- a/src/HOL/Complex/ex/linreif.ML	Sat May 17 23:53:20 2008 +0200
     2.2 +++ b/src/HOL/Complex/ex/linreif.ML	Sun May 18 15:04:09 2008 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4          | _ => error "num_of_term: unsupported Multiplication")
     2.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     2.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     2.7 -      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
     2.8 +      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
     2.9  
    2.10  (* pseudo reification : term -> fm *)
    2.11  fun fm_of_term vs t = 
    2.12 @@ -56,7 +56,7 @@
    2.13  	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    2.14        | Const("All",_)$Term.Abs(xn,xT,p) => 
    2.15  	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    2.16 -      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
    2.17 +      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
    2.18  
    2.19  
    2.20  fun start_vs t =
     3.1 --- a/src/HOL/Complex/ex/linrtac.ML	Sat May 17 23:53:20 2008 +0200
     3.2 +++ b/src/HOL/Complex/ex/linrtac.ML	Sun May 18 15:04:09 2008 +0200
     3.3 @@ -91,7 +91,7 @@
     3.4      let val pth = linr_oracle thy (Pattern.eta_long [] t1)
     3.5      in 
     3.6            (trace_msg ("calling procedure with term:\n" ^
     3.7 -             Sign.string_of_term thy t1);
     3.8 +             Syntax.string_of_term ctxt t1);
     3.9             ((pth RS iffD2) RS pre_thm,
    3.10              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
    3.11      end
     4.1 --- a/src/HOL/Complex/ex/mireif.ML	Sat May 17 23:53:20 2008 +0200
     4.2 +++ b/src/HOL/Complex/ex/mireif.ML	Sun May 18 15:04:09 2008 +0200
     4.3 @@ -34,7 +34,7 @@
     4.4        | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
     4.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     4.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     4.7 -      | _ => error ("num_of_term: unknown term " ^ Sign.string_of_term CPure.thy t);
     4.8 +      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
     4.9          
    4.10  
    4.11  (* pseudo reification : term -> fm *)
    4.12 @@ -58,7 +58,7 @@
    4.13          E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    4.14        | Const("All",_)$Abs(xn,xT,p) => 
    4.15          A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
    4.16 -      | _ => error ("fm_of_term : unknown term!" ^ Sign.string_of_term CPure.thy t);
    4.17 +      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
    4.18  
    4.19  fun start_vs t =
    4.20      let val fs = term_frees t
     5.1 --- a/src/HOL/Complex/ex/mirtac.ML	Sat May 17 23:53:20 2008 +0200
     5.2 +++ b/src/HOL/Complex/ex/mirtac.ML	Sun May 18 15:04:09 2008 +0200
     5.3 @@ -138,7 +138,7 @@
     5.4  	     else mirlfr_oracle sg (Pattern.eta_long [] t1)
     5.5      in 
     5.6            (trace_msg ("calling procedure with term:\n" ^
     5.7 -             Sign.string_of_term sg t1);
     5.8 +             Syntax.string_of_term ctxt t1);
     5.9             ((pth RS iffD2) RS pre_thm,
    5.10              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
    5.11      end
     6.1 --- a/src/HOL/Import/proof_kernel.ML	Sat May 17 23:53:20 2008 +0200
     6.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun May 18 15:04:09 2008 +0200
     6.3 @@ -246,7 +246,7 @@
     6.4  
     6.5  fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th)
     6.6  fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct)
     6.7 -fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ());
     6.8 +fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ());
     6.9  fun pth (HOLThm(ren,thm)) =
    6.10      let
    6.11          (*val _ = writeln "Renaming:"
     7.1 --- a/src/HOL/Import/shuffler.ML	Sat May 17 23:53:20 2008 +0200
     7.2 +++ b/src/HOL/Import/shuffler.ML	Sun May 18 15:04:09 2008 +0200
     7.3 @@ -48,11 +48,11 @@
     7.4            List.app (writeln o Context.str_of_thy) thys)
     7.5     | TERM (msg,ts) =>
     7.6           (writeln ("Exception TERM raised:\n" ^ msg);
     7.7 -          List.app (writeln o Sign.string_of_term sign) ts)
     7.8 +          List.app (writeln o Syntax.string_of_term_global sign) ts)
     7.9     | TYPE (msg,Ts,ts) =>
    7.10           (writeln ("Exception TYPE raised:\n" ^ msg);
    7.11 -          List.app (writeln o Sign.string_of_typ sign) Ts;
    7.12 -          List.app (writeln o Sign.string_of_term sign) ts)
    7.13 +          List.app (writeln o Syntax.string_of_typ_global sign) Ts;
    7.14 +          List.app (writeln o Syntax.string_of_term_global sign) ts)
    7.15     | e => raise e
    7.16  
    7.17  (*Prints an exception, then fails*)
     8.1 --- a/src/HOL/Library/Eval_Witness.thy	Sat May 17 23:53:20 2008 +0200
     8.2 +++ b/src/HOL/Library/Eval_Witness.thy	Sun May 18 15:04:09 2008 +0200
     8.3 @@ -51,7 +51,7 @@
     8.4    fun check_type T = 
     8.5      if Sorts.of_sort (Sign.classes_of thy) (T, ["Eval_Witness.ml_equiv"])
     8.6      then T
     8.7 -    else error ("Type " ^ quote (Sign.string_of_typ thy T) ^ " not allowed for ML witnesses")
     8.8 +    else error ("Type " ^ quote (Syntax.string_of_typ_global thy T) ^ " not allowed for ML witnesses")
     8.9  
    8.10    fun dest_exs  0 t = t
    8.11      | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
     9.1 --- a/src/HOL/Library/comm_ring.ML	Sat May 17 23:53:20 2008 +0200
     9.2 +++ b/src/HOL/Library/comm_ring.ML	Sun May 18 15:04:09 2008 +0200
     9.3 @@ -77,7 +77,7 @@
     9.4            val crhs = cterm_of thy (reif_polex T fs rhs);
     9.5            val ca = ctyp_of thy T;
     9.6          in (ca, cvs, clhs, crhs) end
     9.7 -      else raise CRing ("reif_eq: not an equation over " ^ Sign.string_of_sort thy cr_sort)
     9.8 +      else raise CRing ("reif_eq: not an equation over " ^ Syntax.string_of_sort_global thy cr_sort)
     9.9    | reif_eq _ _ = raise CRing "reif_eq: not an equation";
    9.10  
    9.11  (* The cring tactic *)
    10.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Sat May 17 23:53:20 2008 +0200
    10.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Sun May 18 15:04:09 2008 +0200
    10.3 @@ -33,7 +33,7 @@
    10.4  oracle mc_eindhoven_oracle ("term") =
    10.5  {*
    10.6  let
    10.7 -  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Sign.string_of_term;
    10.8 +  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
    10.9  
   10.10    fun call_mc s =
   10.11      let
    11.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Sat May 17 23:53:20 2008 +0200
    11.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 15:04:09 2008 +0200
    11.3 @@ -197,8 +197,8 @@
    11.4    | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
    11.5    | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
    11.6      let val thy = theory_of_thm t;
    11.7 -	val fnam = Sign.string_of_term thy (getfun LHS);
    11.8 -	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
    11.9 +	val fnam = Syntax.string_of_term_global thy (getfun LHS);
   11.10 +	val rhs = Syntax.string_of_term_global thy (freeze_thaw RHS)
   11.11  	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
   11.12      in
   11.13  	SOME (prove_goal thy gl (fn prems =>
    12.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Sat May 17 23:53:20 2008 +0200
    12.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Sun May 18 15:04:09 2008 +0200
    12.3 @@ -487,7 +487,7 @@
    12.4  fun string_of_terms sign terms =
    12.5  let fun make_string sign [] = "" |
    12.6   	make_string sign (trm::list) =
    12.7 -           Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
    12.8 +           Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
    12.9  in
   12.10    PrintMode.setmp ["Mucke"] (make_string sign) terms
   12.11  end;
   12.12 @@ -689,7 +689,7 @@
   12.13   rc_in_term sg tl  _ l x 0 = rc_in_termlist sg tl l x |
   12.14   rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) |
   12.15   rc_in_term sg _ trm _ _ n =
   12.16 - error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm));
   12.17 + error("malformed term for case-replacement: " ^ (Syntax.string_of_term_global sg trm));
   12.18   val (bv,n) = check_case sg tl (a $ b);
   12.19  in
   12.20   if (bv) then 
   12.21 @@ -992,7 +992,7 @@
   12.22  fun analyze_types sg [] = [] |
   12.23  analyze_types sg [Type(a,[])] =
   12.24  (let
   12.25 - val s = (Sign.string_of_typ sg (Type(a,[])))
   12.26 + val s = (Syntax.string_of_typ_global sg (Type(a,[])))
   12.27  in
   12.28   (if (s="bool") then ([]) else ([Type(a,[])]))
   12.29  end) |
    13.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat May 17 23:53:20 2008 +0200
    13.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun May 18 15:04:09 2008 +0200
    13.3 @@ -614,7 +614,7 @@
    13.4        let
    13.5          fun eqvt_err s = error
    13.6            ("Could not prove equivariance for introduction rule\n" ^
    13.7 -           Sign.string_of_term (theory_of_thm intr)
    13.8 +           Syntax.string_of_term_global (theory_of_thm intr)
    13.9               (Logic.unvarify (prop_of intr)) ^ "\n" ^ s);
   13.10          val res = SUBPROOF (fn {prems, params, ...} =>
   13.11            let
   13.12 @@ -630,7 +630,7 @@
   13.13        in
   13.14          case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of
   13.15            NONE => eqvt_err ("Rule does not match goal\n" ^
   13.16 -            Sign.string_of_term (theory_of_thm st) (hd (prems_of st)))
   13.17 +            Syntax.string_of_term_global (theory_of_thm st) (hd (prems_of st)))
   13.18          | SOME (th, _) => Seq.single th
   13.19        end;
   13.20      val thss = map (fn atom =>
    14.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sat May 17 23:53:20 2008 +0200
    14.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun May 18 15:04:09 2008 +0200
    14.3 @@ -27,7 +27,7 @@
    14.4  
    14.5  fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
    14.6  fun primrec_eq_err thy s eq =
    14.7 -  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
    14.8 +  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
    14.9  
   14.10  
   14.11  (* preprocessing of equations *)
    15.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sat May 17 23:53:20 2008 +0200
    15.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sun May 18 15:04:09 2008 +0200
    15.3 @@ -501,7 +501,7 @@
    15.4       val dummy =
    15.5             if !trace then
    15.6                 writeln ("ORIGINAL PROTO_DEF: " ^
    15.7 -                          Sign.string_of_term thy proto_def)
    15.8 +                          Syntax.string_of_term_global thy proto_def)
    15.9             else ()
   15.10       val R1 = S.rand WFR
   15.11       val corollary' = R.UNDISCH(R.UNDISCH WFREC_THM)
   15.12 @@ -541,7 +541,7 @@
   15.13       val R'abs = S.rand R'
   15.14       val proto_def' = subst_free[(R1,R')] proto_def
   15.15       val dummy = if !trace then writeln ("proto_def' = " ^
   15.16 -                                         Sign.string_of_term
   15.17 +                                         Syntax.string_of_term_global
   15.18                                           thy proto_def')
   15.19                             else ()
   15.20       val {lhs,rhs} = S.dest_eq proto_def'
    16.1 --- a/src/HOL/Tools/datatype_aux.ML	Sat May 17 23:53:20 2008 +0200
    16.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun May 18 15:04:09 2008 +0200
    16.3 @@ -294,7 +294,7 @@
    16.4  fun unfold_datatypes sign orig_descr sorts (dt_info : datatype_info Symtab.table) descr i =
    16.5    let
    16.6      fun typ_error T msg = error ("Non-admissible type expression\n" ^
    16.7 -      Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
    16.8 +      Syntax.string_of_typ_global sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
    16.9  
   16.10      fun get_dt_descr T i tname dts =
   16.11        (case Symtab.lookup dt_info tname of
    17.1 --- a/src/HOL/Tools/datatype_package.ML	Sat May 17 23:53:20 2008 +0200
    17.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun May 18 15:04:09 2008 +0200
    17.3 @@ -563,7 +563,7 @@
    17.4        Variable.importT_thms [induction] (Variable.thm_context induction);
    17.5  
    17.6      fun err t = error ("Ill-formed predicate in induction rule: " ^
    17.7 -      Sign.string_of_term thy1 t);
    17.8 +      Syntax.string_of_term_global thy1 t);
    17.9  
   17.10      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   17.11            ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
    18.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sat May 17 23:53:20 2008 +0200
    18.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun May 18 15:04:09 2008 +0200
    18.3 @@ -210,7 +210,7 @@
    18.4            end)
    18.5              (if is_set then [Mode (([], []), [], [])]
    18.6               else modes_of modes t handle Option =>
    18.7 -               error ("Bad predicate: " ^ Sign.string_of_term thy t))
    18.8 +               error ("Bad predicate: " ^ Syntax.string_of_term_global thy t))
    18.9        | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   18.10            else NONE) ps);
   18.11  
    19.1 --- a/src/HOL/Tools/metis_tools.ML	Sat May 17 23:53:20 2008 +0200
    19.2 +++ b/src/HOL/Tools/metis_tools.ML	Sun May 18 15:04:09 2008 +0200
    19.3 @@ -166,9 +166,9 @@
    19.4      let val trands = terms_of rands
    19.5      in  if length trands = nargs then Term (list_comb(rator, trands))
    19.6          else error
    19.7 -          ("apply_list: wrong number of arguments: " ^ Sign.string_of_term CPure.thy rator ^
    19.8 -            " expected " ^
    19.9 -            Int.toString nargs ^ " received " ^ commas (map (Sign.string_of_term CPure.thy) trands))
   19.10 +          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global CPure.thy rator ^
   19.11 +            " expected " ^ Int.toString nargs ^
   19.12 +            " received " ^ commas (map (Syntax.string_of_term_global CPure.thy) trands))
   19.13      end;
   19.14  
   19.15  (*Instantiate constant c with the supplied types, but if they don't match its declared
    20.1 --- a/src/HOL/Tools/old_primrec_package.ML	Sat May 17 23:53:20 2008 +0200
    20.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Sun May 18 15:04:09 2008 +0200
    20.3 @@ -27,7 +27,7 @@
    20.4  
    20.5  fun primrec_err s = error ("Primrec definition error:\n" ^ s);
    20.6  fun primrec_eq_err thy s eq =
    20.7 -  primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
    20.8 +  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
    20.9  
   20.10  
   20.11  (*the following code ensures that each recursive set always has the
    21.1 --- a/src/HOL/Tools/refute.ML	Sat May 17 23:53:20 2008 +0200
    21.2 +++ b/src/HOL/Tools/refute.ML	Sun May 18 15:04:09 2008 +0200
    21.3 @@ -219,7 +219,7 @@
    21.4      case get_first (fn (_, f) => f thy model args t)
    21.5        (#interpreters (RefuteData.get thy)) of
    21.6        NONE   => raise REFUTE ("interpret",
    21.7 -        "no interpreter for term " ^ quote (Sign.string_of_term thy t))
    21.8 +        "no interpreter for term " ^ quote (Syntax.string_of_term_global thy t))
    21.9      | SOME x => x;
   21.10  
   21.11  (* ------------------------------------------------------------------------- *)
   21.12 @@ -234,7 +234,7 @@
   21.13      case get_first (fn (_, f) => f thy model T intr assignment)
   21.14        (#printers (RefuteData.get thy)) of
   21.15        NONE   => raise REFUTE ("print",
   21.16 -        "no printer for type " ^ quote (Sign.string_of_typ thy T))
   21.17 +        "no printer for type " ^ quote (Syntax.string_of_typ_global thy T))
   21.18      | SOME x => x;
   21.19  
   21.20  (* ------------------------------------------------------------------------- *)
   21.21 @@ -253,7 +253,7 @@
   21.22          "empty universe (no type variables in term)\n"
   21.23        else
   21.24          "Size of types: " ^ commas (map (fn (T, i) =>
   21.25 -          Sign.string_of_typ thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
   21.26 +          Syntax.string_of_typ_global thy T ^ ": " ^ string_of_int i) typs) ^ "\n"
   21.27      val show_consts_msg =
   21.28        if not (!show_consts) andalso Library.exists (is_Const o fst) terms then
   21.29          "set \"show_consts\" to show the interpretation of constants\n"
   21.30 @@ -266,8 +266,8 @@
   21.31          cat_lines (List.mapPartial (fn (t, intr) =>
   21.32            (* print constants only if 'show_consts' is true *)
   21.33            if (!show_consts) orelse not (is_Const t) then
   21.34 -            SOME (Sign.string_of_term thy t ^ ": " ^
   21.35 -              Sign.string_of_term thy
   21.36 +            SOME (Syntax.string_of_term_global thy t ^ ": " ^
   21.37 +              Syntax.string_of_term_global thy
   21.38                  (print thy model (Term.type_of t) intr assignment))
   21.39            else
   21.40              NONE) terms) ^ "\n"
   21.41 @@ -456,7 +456,7 @@
   21.42            (* schematic type variable not instantiated *)
   21.43            raise REFUTE ("monomorphic_term",
   21.44              "no substitution for type variable " ^ fst (fst v) ^
   21.45 -            " in term " ^ Sign.string_of_term CPure.thy t)
   21.46 +            " in term " ^ Syntax.string_of_term_global CPure.thy t)
   21.47          | SOME typ =>
   21.48            typ)) t;
   21.49  
   21.50 @@ -787,7 +787,7 @@
   21.51            TFree (_, sort) => sort
   21.52          | TVar (_, sort)  => sort
   21.53          | _               => raise REFUTE ("collect_axioms", "type " ^
   21.54 -          Sign.string_of_typ thy T ^ " is not a variable"))
   21.55 +          Syntax.string_of_typ_global thy T ^ " is not a variable"))
   21.56        (* obtain axioms for all superclasses *)
   21.57        val superclasses = sort @ (maps (Sign.super_classes thy) sort)
   21.58        (* merely an optimization, because 'collect_this_axiom' disallows *)
   21.59 @@ -807,7 +807,7 @@
   21.60            (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
   21.61          | _ =>
   21.62            raise REFUTE ("collect_axioms", "class axiom " ^ axname ^ " (" ^
   21.63 -            Sign.string_of_term thy ax ^
   21.64 +            Syntax.string_of_term_global thy ax ^
   21.65              ") contains more than one type variable")))
   21.66          class_axioms
   21.67      in
   21.68 @@ -912,7 +912,7 @@
   21.69                val ax_in   = SOME (specialize_type thy (s, T) inclass)
   21.70                  (* type match may fail due to sort constraints *)
   21.71                  handle Type.TYPE_MATCH => NONE
   21.72 -              val ax_1 = Option.map (fn ax => (Sign.string_of_term thy ax, ax))
   21.73 +              val ax_1 = Option.map (fn ax => (Syntax.string_of_term_global thy ax, ax))
   21.74                  ax_in
   21.75                val ax_2 = Option.map (apsnd (specialize_type thy (s, T)))
   21.76                  (get_classdef thy class)
   21.77 @@ -975,7 +975,7 @@
   21.78              val _ = if Library.exists (fn d =>
   21.79                case d of DatatypeAux.DtTFree _ => false | _ => true) typs then
   21.80                raise REFUTE ("ground_types", "datatype argument (for type "
   21.81 -                ^ Sign.string_of_typ thy T ^ ") is not a variable")
   21.82 +                ^ Syntax.string_of_typ_global thy T ^ ") is not a variable")
   21.83              else ()
   21.84              (* required for mutually recursive datatypes; those need to   *)
   21.85              (* be added even if they are an instance of an otherwise non- *)
   21.86 @@ -1160,14 +1160,14 @@
   21.87      fun wrapper () =
   21.88      let
   21.89        val u      = unfold_defs thy t
   21.90 -      val _      = writeln ("Unfolded term: " ^ Sign.string_of_term thy u)
   21.91 +      val _      = writeln ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
   21.92        val axioms = collect_axioms thy u
   21.93        (* Term.typ list *)
   21.94        val types = Library.foldl (fn (acc, t') =>
   21.95          acc union (ground_types thy t')) ([], u :: axioms)
   21.96        val _     = writeln ("Ground types: "
   21.97          ^ (if null types then "none."
   21.98 -           else commas (map (Sign.string_of_typ thy) types)))
   21.99 +           else commas (map (Syntax.string_of_typ_global thy) types)))
  21.100        (* we can only consider fragments of recursive IDTs, so we issue a  *)
  21.101        (* warning if the formula contains a recursive IDT                  *)
  21.102        (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
  21.103 @@ -1256,7 +1256,7 @@
  21.104        (* enter loop with or without time limit *)
  21.105        writeln ("Trying to find a model that "
  21.106          ^ (if negate then "refutes" else "satisfies") ^ ": "
  21.107 -        ^ Sign.string_of_term thy t);
  21.108 +        ^ Syntax.string_of_term_global thy t);
  21.109        if maxtime>0 then (
  21.110          TimeLimit.timeLimit (Time.fromSeconds maxtime)
  21.111            wrapper ()
  21.112 @@ -2041,7 +2041,7 @@
  21.113                  then
  21.114                    raise REFUTE ("IDT_interpreter",
  21.115                      "datatype argument (for type "
  21.116 -                    ^ Sign.string_of_typ thy (Type (s, Ts))
  21.117 +                    ^ Syntax.string_of_typ_global thy (Type (s, Ts))
  21.118                      ^ ") is not a variable")
  21.119                  else ()
  21.120                (* if the model specifies a depth for the current type, *)
  21.121 @@ -2165,7 +2165,7 @@
  21.122                  then
  21.123                    raise REFUTE ("IDT_constructor_interpreter",
  21.124                      "datatype argument (for type "
  21.125 -                    ^ Sign.string_of_typ thy T
  21.126 +                    ^ Syntax.string_of_typ_global thy T
  21.127                      ^ ") is not a variable")
  21.128                  else ()
  21.129                (* decrement depth for the IDT 'T' *)
  21.130 @@ -2225,7 +2225,7 @@
  21.131                  then
  21.132                    raise REFUTE ("IDT_constructor_interpreter",
  21.133                      "datatype argument (for type "
  21.134 -                    ^ Sign.string_of_typ thy (Type (s', Ts'))
  21.135 +                    ^ Syntax.string_of_typ_global thy (Type (s', Ts'))
  21.136                      ^ ") is not a variable")
  21.137                  else ()
  21.138                (* split the constructors into those occuring before/after *)
  21.139 @@ -3282,7 +3282,7 @@
  21.140                case d of DatatypeAux.DtTFree _ => false | _ => true) dtyps
  21.141              then
  21.142                raise REFUTE ("IDT_printer", "datatype argument (for type " ^
  21.143 -                Sign.string_of_typ thy (Type (s, Ts)) ^ ") is not a variable")
  21.144 +                Syntax.string_of_typ_global thy (Type (s, Ts)) ^ ") is not a variable")
  21.145              else ()
  21.146            (* the index of the element in the datatype *)
  21.147            val element = (case intr of
    22.1 --- a/src/HOL/Tools/res_axioms.ML	Sat May 17 23:53:20 2008 +0200
    22.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun May 18 15:04:09 2008 +0200
    22.3 @@ -79,7 +79,7 @@
    22.4                  val extraTs = rhs_extra_types (Ts ---> T) xtp
    22.5                  val _ = if null extraTs then () else
    22.6                     warning ("Skolemization: extra type vars: " ^
    22.7 -                            commas_quote (map (Sign.string_of_typ thy) extraTs));
    22.8 +                            commas_quote (map (Syntax.string_of_typ_global thy) extraTs));
    22.9                  val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
   22.10                  val args = argsx @ args0
   22.11                  val cT = extraTs ---> Ts ---> T
    23.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat May 17 23:53:20 2008 +0200
    23.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sun May 18 15:04:09 2008 +0200
    23.3 @@ -164,8 +164,8 @@
    23.4  		fun resolution (c1, hyps1) (c2, hyps2) =
    23.5  		let
    23.6  			val _ = if !trace_sat then
    23.7 -					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))
    23.8 -						^ ")\nwith clause: " ^ Display.string_of_thm c2 ^ " (hyps: " ^ ML_Syntax.print_list (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2)) ^ ")")
    23.9 +					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))
   23.10 +						^ ")\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)) ^ ")")
   23.11  				else ()
   23.12  
   23.13  			(* the two literals used for resolution *)
   23.14 @@ -191,7 +191,7 @@
   23.15  				(if hyp1_is_neg then c1' else c2')
   23.16  
   23.17  			val _ = if !trace_sat then
   23.18 -					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)) ^ ")")
   23.19 +					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)) ^ ")")
   23.20  				else ()
   23.21  			val _ = inc counter
   23.22  		in
   23.23 @@ -390,7 +390,7 @@
   23.24  			val msg = "SAT solver found a countermodel:\n"
   23.25  				^ (commas
   23.26  					o map (fn (term, idx) =>
   23.27 -						Sign.string_of_term (the_context ()) term ^ ": "
   23.28 +						Syntax.string_of_term_global (the_context ()) term ^ ": "
   23.29  							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
   23.30  					(Termtab.dest atom_table)
   23.31  		in
    24.1 --- a/src/HOL/Tools/specification_package.ML	Sat May 17 23:53:20 2008 +0200
    24.2 +++ b/src/HOL/Tools/specification_package.ML	Sun May 18 15:04:09 2008 +0200
    24.3 @@ -147,9 +147,9 @@
    24.4                  case List.filter (fn t => let val (name,typ) = dest_Const t
    24.5                                       in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
    24.6                                       end) thawed_prop_consts of
    24.7 -                    [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term thy c) ^ "\" found")
    24.8 +                    [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
    24.9                    | [cf] => unvarify cf vmap
   24.10 -                  | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term thy c) ^ "\" found (try applying explicit type constraints)")
   24.11 +                  | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")
   24.12              end
   24.13          val proc_consts = map proc_const consts
   24.14          fun mk_exist (c,prop) =
    25.1 --- a/src/HOL/Tools/typecopy_package.ML	Sat May 17 23:53:20 2008 +0200
    25.2 +++ b/src/HOL/Tools/typecopy_package.ML	Sun May 18 15:04:09 2008 +0200
    25.3 @@ -52,10 +52,10 @@
    25.4      val tab = TypecopyData.get thy;
    25.5      fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
    25.6        (Pretty.block o Pretty.breaks) [
    25.7 -        Sign.pretty_typ thy (Type (tyco, map TFree vs)),
    25.8 +        Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),
    25.9          Pretty.str "=",
   25.10          (Pretty.str o Sign.extern_const thy) constr,
   25.11 -        Sign.pretty_typ thy typ,
   25.12 +        Syntax.pretty_typ_global thy typ,
   25.13          Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];
   25.14      in
   25.15        (Pretty.writeln o Pretty.block o Pretty.fbreaks)
    26.1 --- a/src/HOL/Tools/typedef_package.ML	Sat May 17 23:53:20 2008 +0200
    26.2 +++ b/src/HOL/Tools/typedef_package.ML	Sun May 18 15:04:09 2008 +0200
    26.3 @@ -223,8 +223,9 @@
    26.4      val name = the_default (#1 typ) opt_name;
    26.5      val (set, goal, _, typedef_result) =
    26.6        prepare_typedef prep_term def name typ set opt_morphs thy;
    26.7 -    val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
    26.8 -      cat_error msg ("Failed to prove non-emptiness of " ^ quote (Sign.string_of_term thy set));
    26.9 +    val non_empty = Goal.prove_global thy [] [] goal (K tac)
   26.10 +      handle ERROR msg => cat_error msg
   26.11 +        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   26.12    in typedef_result non_empty thy end;
   26.13  
   26.14  in
    27.1 --- a/src/HOL/ex/svc_funcs.ML	Sat May 17 23:53:20 2008 +0200
    27.2 +++ b/src/HOL/ex/svc_funcs.ML	Sun May 18 15:04:09 2008 +0200
    27.3 @@ -239,7 +239,8 @@
    27.4  
    27.5   (*The oracle proves the given formula t, if possible*)
    27.6   fun oracle thy t =
    27.7 -  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else ();
    27.8 +  (if ! trace then tracing ("SVC oracle: problem is\n" ^ Syntax.string_of_term_global thy t)
    27.9 +   else ();
   27.10     if valid (expr_of false t) then t else fail t);
   27.11  
   27.12  end;
    28.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sat May 17 23:53:20 2008 +0200
    28.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sun May 18 15:04:09 2008 +0200
    28.3 @@ -56,7 +56,7 @@
    28.4  end
    28.5  |
    28.6  IntC sg t =
    28.7 -error("malformed automaton def for IntC:\n" ^ (Sign.string_of_term sg t));
    28.8 +error("malformed automaton def for IntC:\n" ^ (Syntax.string_of_term_global sg t));
    28.9  
   28.10  fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
   28.11  let
   28.12 @@ -67,7 +67,7 @@
   28.13  end
   28.14  |
   28.15  StartC sg t =
   28.16 -error("malformed automaton def for StartC:\n" ^ (Sign.string_of_term sg t));
   28.17 +error("malformed automaton def for StartC:\n" ^ (Syntax.string_of_term_global sg t));
   28.18  
   28.19  fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
   28.20  let
   28.21 @@ -78,7 +78,7 @@
   28.22  end
   28.23  |
   28.24  TransC sg t =
   28.25 -error("malformed automaton def for TransC:\n" ^ (Sign.string_of_term sg t));
   28.26 +error("malformed automaton def for TransC:\n" ^ (Syntax.string_of_term_global sg t));
   28.27  
   28.28  fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
   28.29  let
   28.30 @@ -91,7 +91,7 @@
   28.31  end
   28.32  |
   28.33  IntA sg t =
   28.34 -error("malformed automaton def for IntA:\n" ^ (Sign.string_of_term sg t));
   28.35 +error("malformed automaton def for IntA:\n" ^ (Syntax.string_of_term_global sg t));
   28.36  
   28.37  fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
   28.38  let
   28.39 @@ -102,7 +102,7 @@
   28.40  end
   28.41  |
   28.42  StartA sg t =
   28.43 -error("malformed automaton def for StartA:\n" ^ (Sign.string_of_term sg t));
   28.44 +error("malformed automaton def for StartA:\n" ^ (Syntax.string_of_term_global sg t));
   28.45  
   28.46  fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
   28.47  let
   28.48 @@ -113,7 +113,7 @@
   28.49  end
   28.50  |
   28.51  TransA sg t =
   28.52 -error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
   28.53 +error("malformed automaton def for TransA:\n" ^ (Syntax.string_of_term_global sg t));
   28.54  
   28.55  fun delete_ul [] = []
   28.56  | delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
   28.57 @@ -125,7 +125,7 @@
   28.58  fun delete_ul_string s = implode(delete_ul (explode s));
   28.59  
   28.60  fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   28.61 -type_list_of sign a = [(Sign.string_of_typ sign a)];
   28.62 +type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
   28.63  
   28.64  fun structured_tuple l (Type("*",s::t::_)) =
   28.65  let
   28.66 @@ -182,15 +182,15 @@
   28.67    let
   28.68      val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o DatatypePackage.get_datatypes) sign;
   28.69      val concl = Logic.strip_imp_concl subgoal;
   28.70 -    val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl));
   28.71 -    val ia_str = delete_ul_string(Sign.string_of_term sign (IntA sign concl));
   28.72 -	val sc_str = delete_ul_string(Sign.string_of_term sign (StartC sign concl));	
   28.73 -	val sa_str = delete_ul_string(Sign.string_of_term sign (StartA sign concl));
   28.74 -	val tc_str = delete_ul_string(Sign.string_of_term sign (TransC sign concl));
   28.75 -	val ta_str = delete_ul_string(Sign.string_of_term sign (TransA sign concl));
   28.76 +    val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
   28.77 +    val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));
   28.78 +	val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));	
   28.79 +	val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));
   28.80 +	val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl));
   28.81 +	val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl));
   28.82  	
   28.83  	val action_type_str =
   28.84 -	Sign.string_of_typ sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
   28.85 +	Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
   28.86  
   28.87  	val abs_state_type_list =
   28.88  	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
   28.89 @@ -291,7 +291,7 @@
   28.90  )
   28.91  end)
   28.92  handle malformed =>
   28.93 -error("No suitable match to IOA types in " ^ (Sign.string_of_term sign subgoal));
   28.94 +error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal));
   28.95  
   28.96  end
   28.97  
    29.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sat May 17 23:53:20 2008 +0200
    29.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Sun May 18 15:04:09 2008 +0200
    29.3 @@ -19,8 +19,8 @@
    29.4  structure IoaPackage: IOA_PACKAGE =
    29.5  struct
    29.6  
    29.7 -val string_of_typ = PrintMode.setmp [] o Sign.string_of_typ;
    29.8 -val string_of_term = PrintMode.setmp [] o Sign.string_of_term;
    29.9 +val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
   29.10 +val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
   29.11  
   29.12  exception malformed;
   29.13  
    30.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Sat May 17 23:53:20 2008 +0200
    30.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Sun May 18 15:04:09 2008 +0200
    30.3 @@ -74,7 +74,7 @@
    30.4  in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
    30.5  
    30.6  fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
    30.7 -fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
    30.8 +fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
    30.9  
   30.10  (* ----- constructor list handling ----- *)
   30.11  
    31.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sat May 17 23:53:20 2008 +0200
    31.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sun May 18 15:04:09 2008 +0200
    31.3 @@ -32,7 +32,7 @@
    31.4  
    31.5  fun fixrec_err s = error ("fixrec definition error:\n" ^ s);
    31.6  fun fixrec_eq_err thy s eq =
    31.7 -  fixrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term thy eq));
    31.8 +  fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
    31.9  
   31.10  (* ->> is taken from holcf_logic.ML *)
   31.11  (* TODO: fix dependencies so we can import HOLCFLogic here *)
    32.1 --- a/src/Provers/blast.ML	Sat May 17 23:53:20 2008 +0200
    32.2 +++ b/src/Provers/blast.ML	Sun May 18 15:04:09 2008 +0200
    32.3 @@ -614,7 +614,7 @@
    32.4    | showTerm d (f $ u)       = if d=0 then dummyVar
    32.5                                 else Term.$ (showTerm d f, showTerm (d-1) u);
    32.6  
    32.7 -fun string_of thy d t = Sign.string_of_term thy (showTerm d t);
    32.8 +fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t);
    32.9  
   32.10  (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   32.11    Ex(P) is duplicated as the assumption ~Ex(P). *)
   32.12 @@ -638,7 +638,7 @@
   32.13    in
   32.14        case topType thy t' of
   32.15            NONE   => stm   (*no type to attach*)
   32.16 -        | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ thy T
   32.17 +        | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T
   32.18    end;
   32.19  
   32.20  
    33.1 --- a/src/Pure/Isar/class.ML	Sat May 17 23:53:20 2008 +0200
    33.2 +++ b/src/Pure/Isar/class.ML	Sun May 18 15:04:09 2008 +0200
    33.3 @@ -722,7 +722,7 @@
    33.4      val inst_params = map_product get_param tycos params |> map_filter I;
    33.5      val primary_constraints = map (apsnd
    33.6        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) params;
    33.7 -    val pp = Sign.pp thy;
    33.8 +    val pp = Syntax.pp_global thy;
    33.9      val algebra = Sign.classes_of thy
   33.10        |> fold (fn tyco => Sorts.add_arities pp
   33.11              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
   33.12 @@ -793,7 +793,7 @@
   33.13      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
   33.14      fun pr_param ((c, _), (v, ty)) =
   33.15        (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   33.16 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Sign.pretty_typ thy ty];
   33.17 +        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
   33.18    in
   33.19      (Pretty.block o Pretty.fbreaks)
   33.20        (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
    34.1 --- a/src/Pure/Isar/code_unit.ML	Sat May 17 23:53:20 2008 +0200
    34.2 +++ b/src/Pure/Isar/code_unit.ML	Sun May 18 15:04:09 2008 +0200
    34.3 @@ -62,7 +62,7 @@
    34.4    => (warning ("code generator: " ^ msg); NONE);
    34.5  fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;
    34.6  
    34.7 -fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
    34.8 +fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
    34.9  fun string_of_const thy c = case AxClass.inst_of_param thy c
   34.10   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
   34.11    | NONE => Sign.extern_const thy c;
   34.12 @@ -269,7 +269,7 @@
   34.13  
   34.14  fun check_bare_const thy t = case try dest_Const t
   34.15   of SOME c_ty => c_ty
   34.16 -  | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t);
   34.17 +  | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
   34.18  
   34.19  fun check_const thy = subst_alias thy o AxClass.unoverload_const thy o apfst (subst_alias thy)
   34.20    o check_bare_const thy;
    35.1 --- a/src/Pure/Isar/constdefs.ML	Sat May 17 23:53:20 2008 +0200
    35.2 +++ b/src/Pure/Isar/constdefs.ML	Sun May 18 15:04:09 2008 +0200
    35.3 @@ -25,7 +25,7 @@
    35.4  fun gen_constdef prep_vars prep_prop prep_att
    35.5      structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
    35.6    let
    35.7 -    fun err msg ts = error (cat_lines (msg :: map (Sign.string_of_term thy) ts));
    35.8 +    fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
    35.9  
   35.10      val thy_ctxt = ProofContext.init thy;
   35.11      val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
    36.1 --- a/src/Pure/Isar/overloading.ML	Sat May 17 23:53:20 2008 +0200
    36.2 +++ b/src/Pure/Isar/overloading.ML	Sun May 18 15:04:09 2008 +0200
    36.3 @@ -174,7 +174,7 @@
    36.4      val overloading = get_overloading lthy;
    36.5      fun pr_operation ((c, ty), (v, _)) =
    36.6        (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    36.7 -        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Sign.pretty_typ thy ty];
    36.8 +        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
    36.9    in
   36.10      (Pretty.block o Pretty.fbreaks)
   36.11        (Pretty.str "overloading" :: map pr_operation overloading)
    37.1 --- a/src/Pure/Isar/proof_context.ML	Sat May 17 23:53:20 2008 +0200
    37.2 +++ b/src/Pure/Isar/proof_context.ML	Sun May 18 15:04:09 2008 +0200
    37.3 @@ -284,7 +284,7 @@
    37.4  
    37.5  fun pretty_thm_legacy th =
    37.6    let val thy = Thm.theory_of_thm th
    37.7 -  in Display.pretty_thm_aux (Syntax.pp (init thy)) true false [] th end;
    37.8 +  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
    37.9  
   37.10  fun pretty_thm ctxt th =
   37.11    let val asms = map Thm.term_of (Assumption.assms_of ctxt)
   37.12 @@ -365,7 +365,7 @@
   37.13    (if can Name.dest_skolem x then Pretty.mark Markup.skolem (Pretty.str (revert_skolem ctxt x))
   37.14     else Pretty.mark Markup.free (Pretty.str x))
   37.15    |> Pretty.mark
   37.16 -    (if Variable.is_fixed ctxt x orelse Sign.is_pretty_global ctxt then Markup.fixed x
   37.17 +    (if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt then Markup.fixed x
   37.18       else Markup.hilite);
   37.19  
   37.20  fun var_or_skolem _ s =
    38.1 --- a/src/Pure/Proof/extraction.ML	Sat May 17 23:53:20 2008 +0200
    38.2 +++ b/src/Pure/Proof/extraction.ML	Sun May 18 15:04:09 2008 +0200
    38.3 @@ -278,7 +278,7 @@
    38.4    let
    38.5      val {typeof_eqns, ...} = ExtractionData.get thy;
    38.6      fun err () = error ("Unable to determine type of extracted program for\n" ^
    38.7 -      Sign.string_of_term thy t)
    38.8 +      Syntax.string_of_term_global thy t)
    38.9    in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
   38.10      [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
   38.11        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
   38.12 @@ -582,7 +582,7 @@
   38.13              | SOME rs => (case find vs' rs of
   38.14                  SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
   38.15                | NONE => error ("corr: no realizer for instance of theorem " ^
   38.16 -                  quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   38.17 +                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   38.18                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   38.19            end
   38.20  
   38.21 @@ -596,7 +596,7 @@
   38.22              else case find vs' (Symtab.lookup_list realizers s) of
   38.23                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
   38.24              | NONE => error ("corr: no realizer for instance of axiom " ^
   38.25 -                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   38.26 +                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   38.27                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   38.28            end
   38.29  
   38.30 @@ -691,7 +691,7 @@
   38.31              | SOME rs => (case find vs' rs of
   38.32                  SOME (t, _) => (defs, subst_TVars tye' t)
   38.33                | NONE => error ("extr: no realizer for instance of theorem " ^
   38.34 -                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   38.35 +                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   38.36                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
   38.37            end
   38.38  
   38.39 @@ -703,7 +703,7 @@
   38.40              case find vs' (Symtab.lookup_list realizers s) of
   38.41                SOME (t, _) => (defs, subst_TVars tye' t)
   38.42              | NONE => error ("extr: no realizer for instance of axiom " ^
   38.43 -                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
   38.44 +                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
   38.45                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
   38.46            end
   38.47  
    39.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat May 17 23:53:20 2008 +0200
    39.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun May 18 15:04:09 2008 +0200
    39.3 @@ -171,7 +171,7 @@
    39.4        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
    39.5            (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    39.6        | prf_of _ t = error ("Not a proof term:\n" ^
    39.7 -          Sign.string_of_term thy t)
    39.8 +          Syntax.string_of_term_global thy t)
    39.9  
   39.10    in prf_of [] end;
   39.11  
   39.12 @@ -268,7 +268,7 @@
   39.13    in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
   39.14  
   39.15  fun pretty_proof thy prf =
   39.16 -  Sign.pretty_term (proof_syntax prf thy) (term_of_proof prf);
   39.17 +  Syntax.pretty_term_global (proof_syntax prf thy) (term_of_proof prf);
   39.18  
   39.19  fun pretty_proof_of full thm =
   39.20    pretty_proof (Thm.theory_of_thm thm) (proof_of full thm);
    40.1 --- a/src/Pure/Proof/proofchecker.ML	Sat May 17 23:53:20 2008 +0200
    40.2 +++ b/src/Pure/Proof/proofchecker.ML	Sun May 18 15:04:09 2008 +0200
    40.3 @@ -51,8 +51,8 @@
    40.4              val {prop, ...} = rep_thm thm;
    40.5              val _ = if prop aconv prop' then () else
    40.6                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
    40.7 -                Sign.string_of_term thy prop ^ "\n\n" ^
    40.8 -                Sign.string_of_term thy prop');
    40.9 +                Syntax.string_of_term_global thy prop ^ "\n\n" ^
   40.10 +                Syntax.string_of_term_global thy prop');
   40.11            in thm_of_atom thm Ts end
   40.12  
   40.13        | thm_of _ _ (PAxm (name, _, SOME Ts)) =
    41.1 --- a/src/Pure/Proof/reconstruct.ML	Sat May 17 23:53:20 2008 +0200
    41.2 +++ b/src/Pure/Proof/reconstruct.ML	Sun May 18 15:04:09 2008 +0200
    41.3 @@ -65,7 +65,7 @@
    41.4      val (iTs', maxidx') = Sign.typ_unify thy (T, U) (iTs, maxidx)
    41.5    in Envir.Envir {asol=asol, iTs=iTs', maxidx=maxidx'} end
    41.6    handle Type.TUNIFY => error ("Non-unifiable types:\n" ^
    41.7 -    Sign.string_of_typ thy T ^ "\n\n" ^ Sign.string_of_typ thy U);
    41.8 +    Syntax.string_of_typ_global thy T ^ "\n\n" ^ Syntax.string_of_typ_global thy U);
    41.9  
   41.10  fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) =
   41.11        (case Type.lookup iTs ixnS of NONE => T | SOME T' => chaseT env T')
   41.12 @@ -107,7 +107,7 @@
   41.13        handle Subscript => error ("infer_type: bad variable index " ^ string_of_int i));
   41.14  
   41.15  fun cantunify thy (t, u) = error ("Non-unifiable terms:\n" ^
   41.16 -  Sign.string_of_term thy t ^ "\n\n" ^ Sign.string_of_term thy u);
   41.17 +  Syntax.string_of_term_global thy t ^ "\n\n" ^ Syntax.string_of_term_global thy u);
   41.18  
   41.19  fun decompose thy Ts (env, p as (t, u)) =
   41.20    let fun rigrig (a, T) (b, U) uT ts us = if a <> b then cantunify thy p
   41.21 @@ -264,7 +264,7 @@
   41.22        let
   41.23          fun search env [] = error ("Unsolvable constraints:\n" ^
   41.24                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
   41.25 -                Display.pretty_flexpair (Sign.pp thy) (pairself
   41.26 +                Display.pretty_flexpair (Syntax.pp_global thy) (pairself
   41.27                    (Envir.norm_term bigenv) p)) cs)))
   41.28            | search env ((u, p as (t1, t2), vs)::ps) =
   41.29                if u then
   41.30 @@ -367,7 +367,7 @@
   41.31                  NONE =>
   41.32                    let
   41.33                      val _ = message ("Reconstructing proof of " ^ a);
   41.34 -                    val _ = message (Sign.string_of_term thy prop);
   41.35 +                    val _ = message (Syntax.string_of_term_global thy prop);
   41.36                      val prf' = forall_intr_vfs_prf prop
   41.37                        (reconstruct_proof thy prop cprf);
   41.38                      val (maxidx', prfs', prf) = expand
    42.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat May 17 23:53:20 2008 +0200
    42.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun May 18 15:04:09 2008 +0200
    42.3 @@ -698,7 +698,7 @@
    42.4          fun string_of_thm th = Output.output
    42.5                                 (Pretty.string_of
    42.6                                     (Display.pretty_thm_aux
    42.7 -                                        (Sign.pp (Thm.theory_of_thm th))
    42.8 +                                        (Syntax.pp_global (Thm.theory_of_thm th))
    42.9                                          false (* quote *)
   42.10                                          false (* show hyps *)
   42.11                                          [] (* asms *)
    43.1 --- a/src/Pure/axclass.ML	Sat May 17 23:53:20 2008 +0200
    43.2 +++ b/src/Pure/axclass.ML	Sun May 18 15:04:09 2008 +0200
    43.3 @@ -224,13 +224,14 @@
    43.4  
    43.5  fun cert_classrel thy raw_rel =
    43.6    let
    43.7 +    val string_of_sort = Syntax.string_of_sort_global thy;
    43.8      val (c1, c2) = pairself (Sign.certify_class thy) raw_rel;
    43.9      val _ = Sign.primitive_classrel (c1, c2) (Theory.copy thy);
   43.10      val _ =
   43.11        (case subtract (op =) (all_params_of thy [c1]) (all_params_of thy [c2]) of
   43.12          [] => ()
   43.13 -      | xs => raise TYPE ("Class " ^ Sign.string_of_sort thy [c1] ^ " lacks parameter(s) " ^
   43.14 -          commas_quote xs ^ " of " ^ Sign.string_of_sort thy [c2], [], []));
   43.15 +      | xs => raise TYPE ("Class " ^ string_of_sort [c1] ^ " lacks parameter(s) " ^
   43.16 +          commas_quote xs ^ " of " ^ string_of_sort [c2], [], []));
   43.17    in (c1, c2) end;
   43.18  
   43.19  fun read_classrel thy raw_rel =
   43.20 @@ -314,7 +315,7 @@
   43.21      val tyco = case inst_tyco_of thy (c, T)
   43.22       of SOME tyco => tyco
   43.23        | NONE => error ("Illegal type for instantiation of class parameter: "
   43.24 -        ^ quote (c ^ " :: " ^ Sign.string_of_typ thy T));
   43.25 +        ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
   43.26      val name_inst = instance_name (tyco, class) ^ "_inst";
   43.27      val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
   43.28      val T' = Type.strip_sorts T;
   43.29 @@ -518,7 +519,8 @@
   43.30                | _ => I) typ [];
   43.31          val hyps = vars
   43.32            |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
   43.33 -        val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
   43.34 +        val ths = (typ, sort)
   43.35 +          |> Sorts.of_sort_derivation (Syntax.pp_global thy) (Sign.classes_of thy)
   43.36             {class_relation =
   43.37                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
   43.38              type_constructor =
   43.39 @@ -536,7 +538,7 @@
   43.40      val sort' = filter (is_none o lookup_type cache typ) sort;
   43.41      val ths' = derive_type thy (typ, sort')
   43.42        handle ERROR msg => cat_error msg ("The error(s) above occurred for sort derivation: " ^
   43.43 -        Sign.string_of_typ thy typ ^ " :: " ^ Sign.string_of_sort thy sort');
   43.44 +        Syntax.string_of_typ_global thy typ ^ " :: " ^ Syntax.string_of_sort_global thy sort');
   43.45      val cache' = cache |> fold (insert_type typ) (sort' ~~ ths');
   43.46      val ths =
   43.47        sort |> map (fn c =>
    44.1 --- a/src/Pure/codegen.ML	Sat May 17 23:53:20 2008 +0200
    44.2 +++ b/src/Pure/codegen.ML	Sun May 18 15:04:09 2008 +0200
    44.3 @@ -582,13 +582,13 @@
    44.4  fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first
    44.5     (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
    44.6        NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
    44.7 -        Sign.string_of_term thy t)
    44.8 +        Syntax.string_of_term_global thy t)
    44.9      | SOME x => x);
   44.10  
   44.11  fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first
   44.12     (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
   44.13        NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
   44.14 -        Sign.string_of_typ thy T)
   44.15 +        Syntax.string_of_typ_global thy T)
   44.16      | SOME x => x);
   44.17  
   44.18  
   44.19 @@ -987,10 +987,10 @@
   44.20          let val T = the_default (the_default (TFree p) default_type)
   44.21            (AList.lookup (op =) tvinsts s)
   44.22          in if Sign.of_sort thy (T, S) then T
   44.23 -          else error ("Type " ^ Sign.string_of_typ thy T ^
   44.24 +          else error ("Type " ^ Syntax.string_of_typ_global thy T ^
   44.25              " to be substituted for variable " ^
   44.26 -            Sign.string_of_typ thy (TFree p) ^ "\ndoes not have sort " ^
   44.27 -            Sign.string_of_sort thy S)
   44.28 +            Syntax.string_of_typ_global thy (TFree p) ^ "\ndoes not have sort " ^
   44.29 +            Syntax.string_of_sort_global thy S)
   44.30          end))
   44.31        (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
   44.32    in test_term thy quiet size iterations gi' end;
    45.1 --- a/src/Pure/display.ML	Sat May 17 23:53:20 2008 +0200
    45.2 +++ b/src/Pure/display.ML	Sun May 18 15:04:09 2008 +0200
    45.3 @@ -86,7 +86,7 @@
    45.4    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    45.5  
    45.6  fun pretty_thm th =
    45.7 -  pretty_thm_aux (Sign.pp (Thm.theory_of_thm th)) true false [] th;
    45.8 +  pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
    45.9  
   45.10  val string_of_thm = Pretty.string_of o pretty_thm;
   45.11  
   45.12 @@ -109,12 +109,12 @@
   45.13  
   45.14  (* other printing commands *)
   45.15  
   45.16 -fun pretty_ctyp cT = Sign.pretty_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   45.17 -fun string_of_ctyp cT = Sign.string_of_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   45.18 +fun pretty_ctyp cT = Syntax.pretty_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   45.19 +fun string_of_ctyp cT = Syntax.string_of_typ_global (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
   45.20  val print_ctyp = writeln o string_of_ctyp;
   45.21  
   45.22 -fun pretty_cterm ct = Sign.pretty_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   45.23 -fun string_of_cterm ct = Sign.string_of_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
   45.24 +fun pretty_cterm ct = Syntax.pretty_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
   45.25 +fun string_of_cterm ct = Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct);
   45.26  val print_cterm = writeln o string_of_cterm;
   45.27  
   45.28  
   45.29 @@ -138,7 +138,7 @@
   45.30      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
   45.31      val prt_term_no_vars = prt_term o Logic.unvarify;
   45.32      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
   45.33 -    val prt_const' = Defs.pretty_const (Sign.pp thy);
   45.34 +    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
   45.35  
   45.36      fun pretty_classrel (c, []) = prt_cls c
   45.37        | pretty_classrel (c, cs) = Pretty.block
   45.38 @@ -326,7 +326,7 @@
   45.39    end;
   45.40  
   45.41  fun pretty_goals n th =
   45.42 -  pretty_goals_aux (Sign.pp (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   45.43 +  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
   45.44  
   45.45  val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
   45.46  
    46.1 --- a/src/Pure/drule.ML	Sat May 17 23:53:20 2008 +0200
    46.2 +++ b/src/Pure/drule.ML	Sun May 18 15:04:09 2008 +0200
    46.3 @@ -826,12 +826,12 @@
    46.4          val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
    46.5          val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
    46.6            handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
    46.7 -            Sign.string_of_typ thy' (Envir.norm_type tye T) ^
    46.8 +            Syntax.string_of_typ_global thy' (Envir.norm_type tye T) ^
    46.9              "\nof variable " ^
   46.10 -            Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^
   46.11 +            Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) t) ^
   46.12              "\ncannot be unified with type\n" ^
   46.13 -            Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^
   46.14 -            Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u),
   46.15 +            Syntax.string_of_typ_global thy' (Envir.norm_type tye U) ^ "\nof term " ^
   46.16 +            Syntax.string_of_term_global thy' (Term.map_types (Envir.norm_type tye) u),
   46.17              [T, U], [t, u])
   46.18      in  (thy', tye', maxi')  end;
   46.19  in
    47.1 --- a/src/Pure/goal.ML	Sat May 17 23:53:20 2008 +0200
    47.2 +++ b/src/Pure/goal.ML	Sun May 18 15:04:09 2008 +0200
    47.3 @@ -107,7 +107,7 @@
    47.4  fun prove_multi ctxt xs asms props tac =
    47.5    let
    47.6      val thy = ProofContext.theory_of ctxt;
    47.7 -    val string_of_term = Sign.string_of_term thy;
    47.8 +    val string_of_term = Syntax.string_of_term ctxt;
    47.9  
   47.10      fun err msg = cat_error msg
   47.11        ("The error(s) above occurred for the goal statement:\n" ^
    48.1 --- a/src/Pure/meta_simplifier.ML	Sat May 17 23:53:20 2008 +0200
    48.2 +++ b/src/Pure/meta_simplifier.ML	Sun May 18 15:04:09 2008 +0200
    48.3 @@ -294,7 +294,7 @@
    48.4  in
    48.5  
    48.6  fun print_term ss warn a thy t = prnt ss warn (a ^ "\n" ^
    48.7 -  Sign.string_of_term thy (if ! debug_simp then t else show_bounds ss t));
    48.8 +  Syntax.string_of_term_global thy (if ! debug_simp then t else show_bounds ss t));
    48.9  
   48.10  fun debug warn a ss = if ! debug_simp then prnt ss warn (a ()) else ();
   48.11  fun trace warn a ss = if ! trace_simp then prnt ss warn (a ()) else ();
    49.1 --- a/src/Pure/old_goals.ML	Sat May 17 23:53:20 2008 +0200
    49.2 +++ b/src/Pure/old_goals.ML	Sun May 18 15:04:09 2008 +0200
    49.3 @@ -182,7 +182,7 @@
    49.4                  (string_of_int ngoals ^ " unsolved goals!")
    49.5              else if not (null hyps) then !result_error_fn state
    49.6                  ("Additional hypotheses:\n" ^
    49.7 -                 cat_lines (map (Sign.string_of_term thy) hyps))
    49.8 +                 cat_lines (map (Syntax.string_of_term_global thy) hyps))
    49.9              else if Pattern.matches thy
   49.10                                      (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
   49.11                   then final_th
   49.12 @@ -207,11 +207,11 @@
   49.13            List.app (writeln o Context.str_of_thy) thys)
   49.14     | TERM (msg,ts) =>
   49.15           (writeln ("Exception TERM raised:\n" ^ msg);
   49.16 -          List.app (writeln o Sign.string_of_term thy) ts)
   49.17 +          List.app (writeln o Syntax.string_of_term_global thy) ts)
   49.18     | TYPE (msg,Ts,ts) =>
   49.19           (writeln ("Exception TYPE raised:\n" ^ msg);
   49.20 -          List.app (writeln o Sign.string_of_typ thy) Ts;
   49.21 -          List.app (writeln o Sign.string_of_term thy) ts)
   49.22 +          List.app (writeln o Syntax.string_of_typ_global thy) Ts;
   49.23 +          List.app (writeln o Syntax.string_of_term_global thy) ts)
   49.24     | e => raise e;
   49.25  
   49.26  (*Prints an exception, then fails*)
    50.1 --- a/src/Pure/pattern.ML	Sat May 17 23:53:20 2008 +0200
    50.2 +++ b/src/Pure/pattern.ML	Sun May 18 15:04:09 2008 +0200
    50.3 @@ -41,16 +41,17 @@
    50.4  
    50.5  val trace_unify_fail = ref false;
    50.6  
    50.7 -fun string_of_term thy env binders t = Sign.string_of_term thy
    50.8 -  (Envir.norm_term env (subst_bounds(map Free binders,t)));
    50.9 +fun string_of_term thy env binders t =
   50.10 +  Syntax.string_of_term_global thy
   50.11 +    (Envir.norm_term env (subst_bounds (map Free binders, t)));
   50.12  
   50.13  fun bname binders i = fst (nth binders i);
   50.14  fun bnames binders is = space_implode " " (map (bname binders) is);
   50.15  
   50.16  fun typ_clash thy (tye,T,U) =
   50.17    if !trace_unify_fail
   50.18 -  then let val t = Sign.string_of_typ thy (Envir.norm_type tye T)
   50.19 -           and u = Sign.string_of_typ thy (Envir.norm_type tye U)
   50.20 +  then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
   50.21 +           and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
   50.22         in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   50.23    else ()
   50.24  
    51.1 --- a/src/Pure/sign.ML	Sat May 17 23:53:20 2008 +0200
    51.2 +++ b/src/Pure/sign.ML	Sun May 18 15:04:09 2008 +0200
    51.3 @@ -61,16 +61,6 @@
    51.4    val intern_term: theory -> term -> term
    51.5    val extern_term: (string -> xstring) -> theory -> term -> term
    51.6    val intern_tycons: theory -> typ -> typ
    51.7 -  val is_pretty_global: Proof.context -> bool
    51.8 -  val set_pretty_global: bool -> Proof.context -> Proof.context
    51.9 -  val init_pretty_global: theory -> Proof.context
   51.10 -  val pretty_term: theory -> term -> Pretty.T
   51.11 -  val pretty_typ: theory -> typ -> Pretty.T
   51.12 -  val pretty_sort: theory -> sort -> Pretty.T
   51.13 -  val string_of_term: theory -> term -> string
   51.14 -  val string_of_typ: theory -> typ -> string
   51.15 -  val string_of_sort: theory -> sort -> string
   51.16 -  val pp: theory -> Pretty.pp
   51.17    val arity_number: theory -> string -> int
   51.18    val arity_sorts: theory -> string -> sort -> sort list
   51.19    val certify_class: theory -> class -> class
   51.20 @@ -329,37 +319,12 @@
   51.21  
   51.22  
   51.23  
   51.24 -(** pretty printing of terms, types etc. **)
   51.25 -
   51.26 -structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
   51.27 -val is_pretty_global = PrettyGlobal.get;
   51.28 -val set_pretty_global = PrettyGlobal.put;
   51.29 -val init_pretty_global = set_pretty_global true o ProofContext.init;
   51.30 -
   51.31 -val pretty_term = Syntax.pretty_term o init_pretty_global;
   51.32 -val pretty_typ = Syntax.pretty_typ o init_pretty_global;
   51.33 -val pretty_sort = Syntax.pretty_sort o init_pretty_global;
   51.34 -
   51.35 -val string_of_term = Syntax.string_of_term o init_pretty_global;
   51.36 -val string_of_typ = Syntax.string_of_typ o init_pretty_global;
   51.37 -val string_of_sort = Syntax.string_of_sort o init_pretty_global;
   51.38 -
   51.39 -(*pp operations -- deferred evaluation*)
   51.40 -fun pp thy = Pretty.pp
   51.41 - (fn x => pretty_term thy x,
   51.42 -  fn x => pretty_typ thy x,
   51.43 -  fn x => pretty_sort thy x,
   51.44 -  fn x => Syntax.pretty_classrel (init_pretty_global thy) x,
   51.45 -  fn x => Syntax.pretty_arity (init_pretty_global thy) x);
   51.46 -
   51.47 -
   51.48 -
   51.49  (** certify entities **)    (*exception TYPE*)
   51.50  
   51.51  (* certify wrt. type signature *)
   51.52  
   51.53  val arity_number = Type.arity_number o tsig_of;
   51.54 -fun arity_sorts thy = Type.arity_sorts (pp thy) (tsig_of thy);
   51.55 +fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
   51.56  
   51.57  val certify_class         = Type.cert_class o tsig_of;
   51.58  val certify_sort          = Type.cert_sort o tsig_of;
   51.59 @@ -416,10 +381,10 @@
   51.60      val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   51.61    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   51.62  
   51.63 -fun certify_term thy = certify' false (pp thy) true (consts_of thy) thy;
   51.64 -fun certify_prop thy = certify' true (pp thy) true (consts_of thy) thy;
   51.65 +fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
   51.66 +fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
   51.67  
   51.68 -fun cert_term_abbrev thy = #1 o certify' false (pp thy) false (consts_of thy) thy;
   51.69 +fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
   51.70  val cert_term = #1 oo certify_term;
   51.71  val cert_prop = #1 oo certify_prop;
   51.72  
   51.73 @@ -460,7 +425,7 @@
   51.74  
   51.75  fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
   51.76    let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
   51.77 -  in Type.add_arity (pp thy) arity (tsig_of thy); arity end;
   51.78 +  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
   51.79  
   51.80  val read_arity = prep_arity intern_type Syntax.read_sort_global;
   51.81  val cert_arity = prep_arity (K I) certify_sort;
   51.82 @@ -547,7 +512,7 @@
   51.83  
   51.84  fun read_def_terms (thy, types, sorts) used freeze sTs =
   51.85    let
   51.86 -    val pp = pp thy;
   51.87 +    val pp = Syntax.pp_global thy;
   51.88      val consts = consts_of thy;
   51.89      val cert_consts = Consts.certify pp (tsig_of thy) true consts;
   51.90      fun map_free x = if is_some (types (x, ~1)) then SOME x else NONE;
   51.91 @@ -678,7 +643,7 @@
   51.92  
   51.93  fun add_abbrev mode tags (c, raw_t) thy =
   51.94    let
   51.95 -    val pp = pp thy;
   51.96 +    val pp = Syntax.pp_global thy;
   51.97      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
   51.98      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   51.99        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c);
  51.100 @@ -706,12 +671,12 @@
  51.101    thy |> map_sign (fn (naming, syn, tsig, consts) =>
  51.102      let
  51.103        val syn' = Syntax.update_consts [bclass] syn;
  51.104 -      val tsig' = Type.add_class (pp thy) naming (bclass, classes) tsig;
  51.105 +      val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
  51.106      in (naming, syn', tsig', consts) end)
  51.107    |> add_consts_i [(Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  51.108  
  51.109 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (pp thy) arg);
  51.110 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (pp thy) arg);
  51.111 +fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
  51.112 +fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
  51.113  
  51.114  
  51.115  (* add translation functions *)
    52.1 --- a/src/Pure/tctical.ML	Sat May 17 23:53:20 2008 +0200
    52.2 +++ b/src/Pure/tctical.ML	Sun May 18 15:04:09 2008 +0200
    52.3 @@ -488,7 +488,7 @@
    52.4  
    52.5  fun print_vars_terms thy (n,thm) =
    52.6    let
    52.7 -    fun typed ty = " has type: " ^ Sign.string_of_typ thy ty;
    52.8 +    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
    52.9      fun find_vars thy (Const (c, ty)) =
   52.10          (case Term.typ_tvars ty
   52.11           of [] => I
    53.1 --- a/src/Pure/theory.ML	Sat May 17 23:53:20 2008 +0200
    53.2 +++ b/src/Pure/theory.ML	Sun May 18 15:04:09 2008 +0200
    53.3 @@ -162,7 +162,7 @@
    53.4  
    53.5  fun begin_theory name imports =
    53.6    let
    53.7 -    val thy = Context.begin_thy Sign.pp name imports;
    53.8 +    val thy = Context.begin_thy Syntax.pp_global name imports;
    53.9      val wrappers = begin_wrappers thy;
   53.10    in thy |> Sign.local_path |> apply_wrappers wrappers end;
   53.11  
   53.12 @@ -185,7 +185,7 @@
   53.13          | TERM (msg, _) => error msg;
   53.14    in
   53.15      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   53.16 -    (name, Sign.no_vars (Sign.pp thy) t)
   53.17 +    (name, Sign.no_vars (Syntax.pp_global thy) t)
   53.18    end;
   53.19  
   53.20  fun read_axm thy (name, str) =
   53.21 @@ -219,7 +219,7 @@
   53.22  
   53.23  fun dependencies thy unchecked is_def name lhs rhs =
   53.24    let
   53.25 -    val pp = Sign.pp thy;
   53.26 +    val pp = Syntax.pp_global thy;
   53.27      val consts = Sign.consts_of thy;
   53.28      fun prep const =
   53.29        let val Const (c, T) = Sign.no_vars pp (Const const)
   53.30 @@ -256,7 +256,7 @@
   53.31  
   53.32      fun message txt =
   53.33        [Pretty.block [Pretty.str "Specification of constant ",
   53.34 -        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ thy T)],
   53.35 +        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
   53.36          Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   53.37    in
   53.38      if Sign.typ_instance thy (declT, T') then ()
   53.39 @@ -281,7 +281,7 @@
   53.40    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   53.41    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   53.42     [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   53.43 -    Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
   53.44 +    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
   53.45  
   53.46  
   53.47  (* add_defs(_i) *)
    54.1 --- a/src/Pure/thm.ML	Sat May 17 23:53:20 2008 +0200
    54.2 +++ b/src/Pure/thm.ML	Sun May 18 15:04:09 2008 +0200
    54.3 @@ -991,13 +991,13 @@
    54.4  
    54.5  local
    54.6  
    54.7 -fun pretty_typing thy t T =
    54.8 -  Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
    54.9 +fun pretty_typing thy t T = Pretty.block
   54.10 +  [Syntax.pretty_term_global thy t, Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ_global thy T];
   54.11  
   54.12  fun add_inst (ct, cu) (thy_ref, sorts) =
   54.13    let
   54.14 -    val Cterm {t = t, T = T, ...} = ct
   54.15 -    and Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
   54.16 +    val Cterm {t = t, T = T, ...} = ct;
   54.17 +    val Cterm {t = u, T = U, sorts = sorts_u, maxidx = maxidx_u, ...} = cu;
   54.18      val thy_ref' = Theory.merge_refs (thy_ref, merge_thys0 ct cu);
   54.19      val sorts' = Sorts.union sorts_u sorts;
   54.20    in
   54.21 @@ -1009,7 +1009,7 @@
   54.22          Pretty.fbrk, pretty_typing (Theory.deref thy_ref') u U]), [T, U], [t, u])
   54.23      | _ => raise TYPE (Pretty.string_of (Pretty.block
   54.24         [Pretty.str "instantiate: not a variable",
   54.25 -        Pretty.fbrk, Sign.pretty_term (Theory.deref thy_ref') t]), [], [t]))
   54.26 +        Pretty.fbrk, Syntax.pretty_term_global (Theory.deref thy_ref') t]), [], [t]))
   54.27    end;
   54.28  
   54.29  fun add_instT (cT, cU) (thy_ref, sorts) =
   54.30 @@ -1021,10 +1021,10 @@
   54.31    in
   54.32      (case T of TVar (v as (_, S)) =>
   54.33        if Sign.of_sort thy' (U, S) then ((v, (U, maxidx_U)), (Theory.check_thy thy', sorts'))
   54.34 -      else raise TYPE ("Type not of sort " ^ Sign.string_of_sort thy' S, [U], [])
   54.35 +      else raise TYPE ("Type not of sort " ^ Syntax.string_of_sort_global thy' S, [U], [])
   54.36      | _ => raise TYPE (Pretty.string_of (Pretty.block
   54.37          [Pretty.str "instantiate: not a type variable",
   54.38 -         Pretty.fbrk, Sign.pretty_typ thy' T]), [T], []))
   54.39 +         Pretty.fbrk, Syntax.pretty_typ_global thy' T]), [T], []))
   54.40    end;
   54.41  
   54.42  in
    55.1 --- a/src/Pure/unify.ML	Sat May 17 23:53:20 2008 +0200
    55.2 +++ b/src/Pure/unify.ML	Sun May 18 15:04:09 2008 +0200
    55.3 @@ -194,7 +194,7 @@
    55.4         handle Type.TUNIFY => raise CANTUNIFY;
    55.5  
    55.6  fun test_unify_types thy (args as (T,U,_)) =
    55.7 -let val str_of = Sign.string_of_typ thy;
    55.8 +let val str_of = Syntax.string_of_typ_global thy;
    55.9      fun warn() = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
   55.10      val env' = unify_types thy args
   55.11  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
   55.12 @@ -556,7 +556,7 @@
   55.13      t is always flexible.*)
   55.14  fun print_dpairs thy msg (env,dpairs) =
   55.15    let fun pdp (rbinder,t,u) =
   55.16 -        let fun termT t = Sign.pretty_term thy
   55.17 +        let fun termT t = Syntax.pretty_term_global thy
   55.18                                (Envir.norm_term env (Logic.rlist_abs(rbinder,t)))
   55.19              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
   55.20                            termT t];
    56.1 --- a/src/Tools/code/code_funcgr.ML	Sat May 17 23:53:20 2008 +0200
    56.2 +++ b/src/Tools/code/code_funcgr.ML	Sun May 18 15:04:09 2008 +0200
    56.3 @@ -73,7 +73,7 @@
    56.4        | mk_inst ty (TFree (_, sort)) = cons (ty, sort)
    56.5        | mk_inst (Type (_, tys1)) (Type (_, tys2)) = fold2 mk_inst tys1 tys2;
    56.6      fun of_sort_deriv (ty, sort) =
    56.7 -      Sorts.of_sort_derivation (Sign.pp thy) algebra
    56.8 +      Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
    56.9          { class_relation = class_relation, type_constructor = type_constructor,
   56.10            type_variable = type_variable }
   56.11          (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
   56.12 @@ -108,7 +108,7 @@
   56.13    | resort_thms algebra tap_typ (thms as thm :: _) =
   56.14        let
   56.15          val thy = Thm.theory_of_thm thm;
   56.16 -        val pp = Sign.pp thy;
   56.17 +        val pp = Syntax.pp_global thy;
   56.18          val cs = fold_consts (insert (op =)) thms [];
   56.19          fun match_const c (ty, ty_decl) =
   56.20            let
   56.21 @@ -279,7 +279,7 @@
   56.22  fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
   56.23    let
   56.24      val ct = cterm_of proto_ct;
   56.25 -    val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
   56.26 +    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
   56.27      val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
   56.28      fun consts_of t = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
   56.29        t [];
    57.1 --- a/src/Tools/code/code_package.ML	Sat May 17 23:53:20 2008 +0200
    57.2 +++ b/src/Tools/code/code_package.ML	Sun May 18 15:04:09 2008 +0200
    57.3 @@ -125,7 +125,7 @@
    57.4  fun eval evaluate term_of reff thy ct args =
    57.5    let
    57.6      val _ = if null (term_frees (term_of ct)) then () else error ("Term "
    57.7 -      ^ quote (Sign.string_of_term thy (term_of ct))
    57.8 +      ^ quote (Syntax.string_of_term_global thy (term_of ct))
    57.9        ^ " to be evaluated contains free variables");
   57.10    in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end;
   57.11  
    58.1 --- a/src/Tools/code/code_thingol.ML	Sat May 17 23:53:20 2008 +0200
    58.2 +++ b/src/Tools/code/code_thingol.ML	Sun May 18 15:04:09 2008 +0200
    58.3 @@ -430,7 +430,7 @@
    58.4        #>> (fn (tyco, tys) => tyco `%% tys)
    58.5  and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
    58.6    let
    58.7 -    val pp = Sign.pp thy;
    58.8 +    val pp = Syntax.pp_global thy;
    58.9      datatype typarg =
   58.10          Global of (class * string) * typarg list list
   58.11        | Local of (class * class) list * (string * (int * sort));
    59.1 --- a/src/ZF/Datatype_ZF.thy	Sat May 17 23:53:20 2008 +0200
    59.2 +++ b/src/ZF/Datatype_ZF.thy	Sun May 18 15:04:09 2008 +0200
    59.3 @@ -97,7 +97,7 @@
    59.4           (fn _ => rtac iff_reflection 1 THEN
    59.5             simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
    59.6           handle ERROR msg =>
    59.7 -         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
    59.8 +         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term_global sg goal);
    59.9            raise Match)
   59.10     in SOME thm end
   59.11     handle Match => NONE;
    60.1 --- a/src/ZF/Tools/datatype_package.ML	Sat May 17 23:53:20 2008 +0200
    60.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun May 18 15:04:09 2008 +0200
    60.3 @@ -54,7 +54,7 @@
    60.4      let val rec_hds = map head_of rec_tms
    60.5          val dummy = assert_all is_Const rec_hds
    60.6            (fn t => "Datatype set not previously declared as constant: " ^
    60.7 -                   Sign.string_of_term @{theory IFOL} t);
    60.8 +                   Syntax.string_of_term_global @{theory IFOL} t);
    60.9          val rec_names = (*nat doesn't have to be added*)
   60.10  	    @{const_name nat} :: map (#1 o dest_Const) rec_hds
   60.11  	val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
   60.12 @@ -72,7 +72,7 @@
   60.13  
   60.14    val dummy = assert_all is_Const rec_hds
   60.15            (fn t => "Datatype set not previously declared as constant: " ^
   60.16 -                   Sign.string_of_term thy t);
   60.17 +                   Syntax.string_of_term_global thy t);
   60.18  
   60.19    val rec_names = map (#1 o dest_Const) rec_hds
   60.20    val rec_base_names = map Sign.base_name rec_names
    61.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat May 17 23:53:20 2008 +0200
    61.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun May 18 15:04:09 2008 +0200
    61.3 @@ -120,7 +120,7 @@
    61.4      (*analyze the LHS of a case equation to get a constructor*)
    61.5      fun const_of (Const("op =", _) $ (_ $ c) $ _) = c
    61.6        | const_of eqn = error ("Ill-formed case equation: " ^
    61.7 -                              Sign.string_of_term thy eqn);
    61.8 +                              Syntax.string_of_term_global thy eqn);
    61.9  
   61.10      val constructors =
   61.11          map (head_of o const_of o FOLogic.dest_Trueprop o
    62.1 --- a/src/ZF/Tools/primrec_package.ML	Sat May 17 23:53:20 2008 +0200
    62.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun May 18 15:04:09 2008 +0200
    62.3 @@ -24,7 +24,7 @@
    62.4  fun primrec_err s = error ("Primrec definition error:\n" ^ s);
    62.5  
    62.6  fun primrec_eq_err sign s eq =
    62.7 -  primrec_err (s ^ "\nin equation\n" ^ Sign.string_of_term sign eq);
    62.8 +  primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq);
    62.9  
   62.10  
   62.11  (* preprocessing of equations *)
   62.12 @@ -125,8 +125,8 @@
   62.13        in
   62.14            if !Ind_Syntax.trace then
   62.15                writeln ("recursor_rhs = " ^
   62.16 -                       Sign.string_of_term thy recursor_rhs ^
   62.17 -                       "\nabs = " ^ Sign.string_of_term thy abs)
   62.18 +                       Syntax.string_of_term_global thy recursor_rhs ^
   62.19 +                       "\nabs = " ^ Syntax.string_of_term_global thy abs)
   62.20            else();
   62.21            if Logic.occs (fconst, abs) then
   62.22                primrec_eq_err thy
   62.23 @@ -152,7 +152,7 @@
   62.24    in
   62.25        if !Ind_Syntax.trace then
   62.26              writeln ("primrec def:\n" ^
   62.27 -                     Sign.string_of_term thy def_tm)
   62.28 +                     Syntax.string_of_term_global thy def_tm)
   62.29        else();
   62.30        (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
   62.31         def_tm)
    63.1 --- a/src/ZF/ind_syntax.ML	Sat May 17 23:53:20 2008 +0200
    63.2 +++ b/src/ZF/ind_syntax.ML	Sun May 18 15:04:09 2008 +0200
    63.3 @@ -13,7 +13,7 @@
    63.4  val trace = ref false;
    63.5  
    63.6  fun traceIt msg thy t =
    63.7 -  if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
    63.8 +  if !trace then (tracing (msg ^ Syntax.string_of_term_global thy t); t)
    63.9    else t;
   63.10  
   63.11  
   63.12 @@ -46,7 +46,7 @@
   63.13  (*As above, but return error message if bad*)
   63.14  fun rule_concl_msg sign rl = rule_concl rl
   63.15      handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
   63.16 -                          Sign.string_of_term sign rl);
   63.17 +                          Syntax.string_of_term_global sign rl);
   63.18  
   63.19  (*For deriving cases rules.  CollectD2 discards the domain, which is redundant;
   63.20    read_instantiate replaces a propositional variable by a formula variable*)