--- 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 =
--- 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 =
--- 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
--- 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
--- 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
--- 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:"
--- 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*)
--- 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)) =
--- 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 *)
--- 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
--- 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 =>
--- 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) |
--- 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 =>
--- 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 *)
--- 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'
--- 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
--- 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)
--- 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);
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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) =
--- 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)
--- 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
--- 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;
--- 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
--- 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;
--- 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 ----- *)
--- 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 *)
--- 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;
--- 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)
--- 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;
--- 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);
--- 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)
--- 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 =
--- 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
--- 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);
--- 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)) =
--- 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
--- 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 *)
--- 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 =>
--- 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;
--- 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;
--- 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
--- 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" ^
--- 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 ();
--- 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*)
--- 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 ()
--- 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 *)
--- 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
--- 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) *)
--- 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
--- 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];
--- 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 [];
--- 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;
--- 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));
--- 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;
--- 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
--- 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
--- 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)
--- 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*)