1.1 --- a/NEWS Mon Oct 08 22:06:32 2007 +0200
1.2 +++ b/NEWS Tue Oct 09 00:20:13 2007 +0200
1.3 @@ -1307,6 +1307,13 @@
1.4 (Syntax.read_term etc.). These supersede former Sign.read_term etc.
1.5 which are considered legacy and await removal.
1.6
1.7 +* Pure/Syntax: generic interfaces for type unchecking
1.8 +(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
1.9 +with common combinations (Syntax.pretty_term, Syntax.string_of_term
1.10 +etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still
1.11 +available for convenience, but refer to the very same operations
1.12 +(using a mere theory instead of a full context).
1.13 +
1.14 * Isar: simplified treatment of user-level errors, using exception
1.15 ERROR of string uniformly. Function error now merely raises ERROR,
1.16 without any side effect on output channels. The Isar toplevel takes
2.1 --- a/doc-src/antiquote_setup.ML Mon Oct 08 22:06:32 2007 +0200
2.2 +++ b/doc-src/antiquote_setup.ML Tue Oct 09 00:20:13 2007 +0200
2.3 @@ -76,7 +76,7 @@
2.4 #> space_implode "\\par\\smallskip%\n"
2.5 #> enclose "\\isa{" "}");
2.6
2.7 -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
2.8 +fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
2.9 fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
2.10
2.11 in
3.1 --- a/src/HOL/Algebra/ringsimp.ML Mon Oct 08 22:06:32 2007 +0200
3.2 +++ b/src/HOL/Algebra/ringsimp.ML Tue Oct 09 00:20:13 2007 +0200
3.3 @@ -34,7 +34,7 @@
3.4 fun print_structures ctxt =
3.5 let
3.6 val structs = Data.get (Context.Proof ctxt);
3.7 - val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
3.8 + val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
3.9 fun pretty_struct ((s, ts), _) = Pretty.block
3.10 [Pretty.str s, Pretty.str ":", Pretty.brk 1,
3.11 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
4.1 --- a/src/HOL/Library/Eval.thy Mon Oct 08 22:06:32 2007 +0200
4.2 +++ b/src/HOL/Library/Eval.thy Tue Oct 09 00:20:13 2007 +0200
4.3 @@ -190,9 +190,9 @@
4.4 of SOME t' => t'
4.5 | NONE => evl thy t;
4.6 val ty' = Term.type_of t';
4.7 - val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
4.8 + val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
4.9 Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
4.10 - Pretty.quote (ProofContext.pretty_typ ctxt ty')];
4.11 + Pretty.quote (Syntax.pretty_typ ctxt ty')];
4.12 in Pretty.writeln p end;
4.13
4.14 val evaluate = gen_evaluate (map snd evaluators);
5.1 --- a/src/HOL/Nominal/nominal_induct.ML Mon Oct 08 22:06:32 2007 +0200
5.2 +++ b/src/HOL/Nominal/nominal_induct.ML Tue Oct 09 00:20:13 2007 +0200
5.3 @@ -134,7 +134,7 @@
5.4 inst >> Option.map (pair NONE);
5.5
5.6 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
5.7 - error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t));
5.8 + error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t));
5.9
5.10 fun unless_more_args scan = Scan.unless (Scan.lift
5.11 ((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
6.1 --- a/src/HOL/Orderings.thy Mon Oct 08 22:06:32 2007 +0200
6.2 +++ b/src/HOL/Orderings.thy Tue Oct 09 00:20:13 2007 +0200
6.3 @@ -275,9 +275,9 @@
6.4 let
6.5 val structs = Data.get (Context.Proof ctxt);
6.6 fun pretty_term t = Pretty.block
6.7 - [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1,
6.8 + [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
6.9 Pretty.str "::", Pretty.brk 1,
6.10 - Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))];
6.11 + Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
6.12 fun pretty_struct ((s, ts), _) = Pretty.block
6.13 [Pretty.str s, Pretty.str ":", Pretty.brk 1,
6.14 Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
7.1 --- a/src/HOL/Tools/datatype_case.ML Mon Oct 08 22:06:32 2007 +0200
7.2 +++ b/src/HOL/Tools/datatype_case.ML Tue Oct 09 00:20:13 2007 +0200
7.3 @@ -247,7 +247,7 @@
7.4 in (pat_rect1, tree)
7.5 end)
7.6 | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
7.7 - ProofContext.string_of_term ctxt t, i)
7.8 + Syntax.string_of_term ctxt t, i)
7.9 end
7.10 | mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
7.11 in mk
7.12 @@ -260,13 +260,13 @@
7.13 (fn x as Free (s, _) => (fn xs =>
7.14 if member op aconv xs x then
7.15 case_error (quote s ^ " occurs repeatedly in the pattern " ^
7.16 - quote (ProofContext.string_of_term ctxt pat))
7.17 + quote (Syntax.string_of_term ctxt pat))
7.18 else x :: xs)
7.19 | _ => I) pat [];
7.20
7.21 fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
7.22 let
7.23 - fun string_of_clause (pat, rhs) = ProofContext.string_of_term ctxt
7.24 + fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
7.25 (Syntax.const "_case1" $ pat $ rhs);
7.26 val _ = map (no_repeat_vars ctxt o fst) clauses;
7.27 val rows = map_index (fn (i, (pat, rhs)) =>
7.28 @@ -333,8 +333,7 @@
7.29 in
7.30 (t' $ u', used'')
7.31 end
7.32 - | prep_pat t used = case_error ("Bad pattern: " ^
7.33 - ProofContext.string_of_term ctxt t);
7.34 + | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
7.35 fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
7.36 let val (l', cnstrts) = strip_constraints l
7.37 in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)
8.1 --- a/src/HOL/Tools/function_package/fundef_common.ML Mon Oct 08 22:06:32 2007 +0200
8.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Oct 09 00:20:13 2007 +0200
8.3 @@ -175,7 +175,7 @@
8.4
8.5 fun split_def ctxt geq =
8.6 let
8.7 - fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
8.8 + fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
8.9 val (qs, imp) = open_all_all geq
8.10
8.11 val gs = Logic.strip_imp_prems imp
8.12 @@ -214,7 +214,7 @@
8.13
8.14 fun check geq =
8.15 let
8.16 - fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
8.17 + fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
8.18
8.19 val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
8.20
9.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Oct 08 22:06:32 2007 +0200
9.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Oct 09 00:20:13 2007 +0200
9.3 @@ -25,7 +25,7 @@
9.4 let
9.5 fun err str = error (cat_lines ["Malformed definition:",
9.6 str ^ " not allowed in sequential mode.",
9.7 - ProofContext.string_of_term ctxt geq])
9.8 + Syntax.string_of_term ctxt geq])
9.9 val thy = ProofContext.theory_of ctxt
9.10
9.11 fun check_constr_pattern (Bound _) = ()
9.12 @@ -235,7 +235,7 @@
9.13
9.14 fun warn_if_redundant ctxt origs tss =
9.15 let
9.16 - fun msg t = "Ignoring redundant equation: " ^ quote (ProofContext.string_of_term ctxt t)
9.17 + fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
9.18
9.19 val (tss', _) = chop (length origs) tss
9.20 fun check ((_, t), []) = (Output.warning (msg t); [])
10.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML Mon Oct 08 22:06:32 2007 +0200
10.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Tue Oct 09 00:20:13 2007 +0200
10.3 @@ -252,7 +252,7 @@
10.4
10.5 fun no_order_msg ctxt table tl measure_funs =
10.6 let
10.7 - val prterm = ProofContext.string_of_term ctxt
10.8 + val prterm = Syntax.string_of_term ctxt
10.9 fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
10.10
10.11 fun pr_goal t i =
10.12 @@ -292,7 +292,7 @@
10.13 val clean_table = map (fn x => map (nth x) order) table
10.14
10.15 val relation = mk_measures domT (map (nth measure_funs) order)
10.16 - val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation))
10.17 + val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
10.18
10.19 in (* 4: proof reconstruction *)
10.20 st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
11.1 --- a/src/HOL/Tools/inductive_package.ML Mon Oct 08 22:06:32 2007 +0200
11.2 +++ b/src/HOL/Tools/inductive_package.ML Tue Oct 09 00:20:13 2007 +0200
11.3 @@ -247,11 +247,11 @@
11.4
11.5 fun err_in_rule ctxt name t msg =
11.6 error (cat_lines ["Ill-formed introduction rule " ^ quote name,
11.7 - ProofContext.string_of_term ctxt t, msg]);
11.8 + Syntax.string_of_term ctxt t, msg]);
11.9
11.10 fun err_in_prem ctxt name t p msg =
11.11 - error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p,
11.12 - "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]);
11.13 + error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
11.14 + "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
11.15
11.16 val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
11.17
11.18 @@ -275,7 +275,7 @@
11.19
11.20 fun check_ind err t = case dest_predicate cs params t of
11.21 NONE => err (bad_app ^
11.22 - commas (map (ProofContext.string_of_term ctxt) params))
11.23 + commas (map (Syntax.string_of_term ctxt) params))
11.24 | SOME (_, _, ys, _) =>
11.25 if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
11.26 then err bad_ind_occ else ();
11.27 @@ -431,7 +431,7 @@
11.28
11.29 fun err msg =
11.30 error (Pretty.string_of (Pretty.block
11.31 - [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
11.32 + [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
11.33
11.34 val elims = Induct.find_casesP ctxt prop;
11.35
12.1 --- a/src/HOL/Tools/lin_arith.ML Mon Oct 08 22:06:32 2007 +0200
12.2 +++ b/src/HOL/Tools/lin_arith.ML Tue Oct 09 00:20:13 2007 +0200
12.3 @@ -656,7 +656,7 @@
12.4 (* implemented above, or 'is_split_thm' should be modified to filter it *)
12.5 (* out *)
12.6 | (t, ts) => (
12.7 - warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^
12.8 + warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
12.9 " (with " ^ string_of_int (length ts) ^
12.10 " argument(s)) not implemented; proof reconstruction is likely to fail");
12.11 NONE
13.1 --- a/src/HOL/Tools/metis_tools.ML Mon Oct 08 22:06:32 2007 +0200
13.2 +++ b/src/HOL/Tools/metis_tools.ML Tue Oct 09 00:20:13 2007 +0200
13.3 @@ -215,9 +215,9 @@
13.4 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
13.5 " but gets " ^ Int.toString (length tys) ^
13.6 " type arguments\n" ^
13.7 - space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^
13.8 + space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
13.9 " the terms are \n" ^
13.10 - space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
13.11 + space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
13.12 end
13.13 | NONE => (*Not a constant. Is it a type constructor?*)
13.14 case Recon.strip_prefix ResClause.tconst_prefix a of
13.15 @@ -236,11 +236,11 @@
13.16 fun fol_terms_to_hol ctxt fol_tms =
13.17 let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
13.18 val _ = Output.debug (fn () => " calling type inference:")
13.19 - val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
13.20 + val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
13.21 val ts' = infer_types ctxt ts;
13.22 val _ = app (fn t => Output.debug
13.23 - (fn () => " final term: " ^ ProofContext.string_of_term ctxt t ^
13.24 - " of type " ^ ProofContext.string_of_typ ctxt (type_of t)))
13.25 + (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
13.26 + " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
13.27 ts'
13.28 in ts' end;
13.29
13.30 @@ -338,7 +338,7 @@
13.31 else
13.32 let
13.33 val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
13.34 - val _ = Output.debug (fn () => " atom: " ^ ProofContext.string_of_term ctxt i_atm)
13.35 + val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
13.36 val prems_th1 = prems_of i_th1
13.37 val prems_th2 = prems_of i_th2
13.38 val index_th1 = get_index (mk_not i_atm) prems_th1
13.39 @@ -373,10 +373,11 @@
13.40 val adjustment = get_ty_arg_size thy tm1
13.41 val p' = if adjustment > p then p else p-adjustment
13.42 val tm_p = List.nth(args,p')
13.43 - handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment ^ " term " ^ ProofContext.string_of_term ctxt tm)
13.44 + handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
13.45 + Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm)
13.46 in
13.47 Output.debug (fn () => "path_finder: " ^ Int.toString p ^
13.48 - " " ^ ProofContext.string_of_term ctxt tm_p);
13.49 + " " ^ Syntax.string_of_term ctxt tm_p);
13.50 if null ps (*FIXME: why not use pattern-matching and avoid repetition*)
13.51 then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
13.52 else let val (r,t) = path_finder_FO tm_p ps
13.53 @@ -398,9 +399,9 @@
13.54 | path_finder_lit tm_a idx = path_finder isFO tm_a idx
13.55 val (tm_subst, body) = path_finder_lit i_atm fp
13.56 val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
13.57 - val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs)
13.58 - val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm)
13.59 - val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst)
13.60 + val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
13.61 + val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
13.62 + val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
13.63 val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
13.64 val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
13.65 val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
14.1 --- a/src/HOL/Tools/res_atp.ML Mon Oct 08 22:06:32 2007 +0200
14.2 +++ b/src/HOL/Tools/res_atp.ML Tue Oct 09 00:20:13 2007 +0200
14.3 @@ -960,8 +960,7 @@
14.4 val thy = ProofContext.theory_of ctxt;
14.5 in
14.6 Output.debug (fn () => "subgoals in isar_atp:\n" ^
14.7 - Pretty.string_of (ProofContext.pretty_term ctxt
14.8 - (Logic.mk_conjunction_list (Thm.prems_of goal))));
14.9 + Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
14.10 Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
14.11 app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
14.12 if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
15.1 --- a/src/HOL/Tools/res_reconstruct.ML Mon Oct 08 22:06:32 2007 +0200
15.2 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 09 00:20:13 2007 +0200
15.3 @@ -352,7 +352,7 @@
15.4 (*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
15.5 ATP may have their literals reordered.*)
15.6 fun isar_lines ctxt ctms =
15.7 - let val string_of = ProofContext.string_of_term ctxt
15.8 + let val string_of = Syntax.string_of_term ctxt
15.9 fun doline have (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
15.10 (case permuted_clause t ctms of
15.11 SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
16.1 --- a/src/HOL/Tools/typedef_package.ML Mon Oct 08 22:06:32 2007 +0200
16.2 +++ b/src/HOL/Tools/typedef_package.ML Tue Oct 09 00:20:13 2007 +0200
16.3 @@ -108,7 +108,7 @@
16.4 val rhs_tfrees = Term.add_tfrees set [];
16.5 val rhs_tfreesT = Term.add_tfreesT setT [];
16.6 val oldT = HOLogic.dest_setT setT handle TYPE _ =>
16.7 - error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
16.8 + error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
16.9 fun mk_nonempty A =
16.10 HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
16.11 val goal = mk_nonempty set;
16.12 @@ -232,7 +232,7 @@
16.13
16.14 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
16.15 let
16.16 - val string_of_term = ProofContext.string_of_term (ProofContext.init thy);
16.17 + val string_of_term = Sign.string_of_term thy;
16.18 val name = the_default (#1 typ) opt_name;
16.19 val (set, goal, _, typedef_result) =
16.20 prepare_typedef prep_term def name typ set opt_morphs thy;
17.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Mon Oct 08 22:06:32 2007 +0200
17.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Oct 09 00:20:13 2007 +0200
17.3 @@ -67,7 +67,7 @@
17.4 val setT = Term.fastype_of set;
17.5 val rhs_tfrees = term_tfrees set;
17.6 val oldT = HOLogic.dest_setT setT handle TYPE _ =>
17.7 - error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
17.8 + error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
17.9 fun mk_nonempty A =
17.10 HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
17.11 fun mk_admissible A =
18.1 --- a/src/Provers/Arith/fast_lin_arith.ML Mon Oct 08 22:06:32 2007 +0200
18.2 +++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 09 00:20:13 2007 +0200
18.3 @@ -416,7 +416,7 @@
18.4 (if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
18.5
18.6 fun trace_term ctxt msg t =
18.7 - (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t)
18.8 + (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
18.9
18.10 fun trace_msg msg =
18.11 if !trace then tracing msg else ();
18.12 @@ -562,7 +562,7 @@
18.13 | (v, lineqs) :: hist' =>
18.14 let
18.15 val frees = map Free params
18.16 - fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t))
18.17 + fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
18.18 val start =
18.19 if v = ~1 then (hist', findex0 discr n lineqs)
18.20 else (hist, replicate n Rat.zero)
19.1 --- a/src/Pure/Isar/args.ML Mon Oct 08 22:06:32 2007 +0200
19.2 +++ b/src/Pure/Isar/args.ML Tue Oct 09 00:20:13 2007 +0200
19.3 @@ -170,8 +170,8 @@
19.4 let
19.5 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
19.6 fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s)
19.7 - | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
19.8 - | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
19.9 + | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T
19.10 + | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t
19.11 | prt (Arg (_, Value (SOME (Fact ths)))) =
19.12 Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
19.13 | prt arg = Pretty.str (string_of arg);
20.1 --- a/src/Pure/Isar/class.ML Mon Oct 08 22:06:32 2007 +0200
20.2 +++ b/src/Pure/Isar/class.ML Tue Oct 09 00:20:13 2007 +0200
20.3 @@ -413,6 +413,8 @@
20.4
20.5 fun print_classes thy =
20.6 let
20.7 + val ctxt = ProofContext.init thy;
20.8 +
20.9 val algebra = Sign.classes_of thy;
20.10 val arities =
20.11 Symtab.empty
20.12 @@ -423,13 +425,13 @@
20.13 fun mk_arity class tyco =
20.14 let
20.15 val Ss = Sorts.mg_domain algebra tyco [class];
20.16 - in Sign.pretty_arity thy (tyco, Ss, [class]) end;
20.17 + in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
20.18 fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
20.19 - ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
20.20 + ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
20.21 fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
20.22 (SOME o Pretty.str) ("class " ^ class ^ ":"),
20.23 (SOME o Pretty.block) [Pretty.str "supersort: ",
20.24 - (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
20.25 + (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
20.26 Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
20.27 ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
20.28 o these o Option.map #params o try (AxClass.get_definition thy)) class,
21.1 --- a/src/Pure/Isar/element.ML Mon Oct 08 22:06:32 2007 +0200
21.2 +++ b/src/Pure/Isar/element.ML Tue Oct 09 00:20:13 2007 +0200
21.3 @@ -164,8 +164,8 @@
21.4
21.5 fun pretty_stmt ctxt =
21.6 let
21.7 - val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
21.8 - val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
21.9 + val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
21.10 + val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
21.11 val prt_terms = separate (Pretty.keyword "and") o map prt_term;
21.12 val prt_name_atts = pretty_name_atts ctxt;
21.13
21.14 @@ -189,8 +189,8 @@
21.15
21.16 fun pretty_ctxt ctxt =
21.17 let
21.18 - val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
21.19 - val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
21.20 + val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
21.21 + val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
21.22 val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
21.23 val prt_name_atts = pretty_name_atts ctxt;
21.24
21.25 @@ -310,7 +310,7 @@
21.26 (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
21.27
21.28 fun pretty_witness ctxt witn =
21.29 - let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in
21.30 + let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
21.31 Pretty.block (prt_term (witness_prop witn) ::
21.32 (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
21.33 (map prt_term (witness_hyps witn))] else []))
22.1 --- a/src/Pure/Isar/find_theorems.ML Mon Oct 08 22:06:32 2007 +0200
22.2 +++ b/src/Pure/Isar/find_theorems.ML Tue Oct 09 00:20:13 2007 +0200
22.3 @@ -40,9 +40,9 @@
22.4 | Elim => Pretty.str (prfx "elim")
22.5 | Dest => Pretty.str (prfx "dest")
22.6 | Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
22.7 - Pretty.quote (ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat))]
22.8 + Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
22.9 | Pattern pat => Pretty.enclose (prfx " \"") "\""
22.10 - [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
22.11 + [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
22.12 end;
22.13
22.14
23.1 --- a/src/Pure/Isar/isar_cmd.ML Mon Oct 08 22:06:32 2007 +0200
23.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 09 00:20:13 2007 +0200
23.3 @@ -562,7 +562,7 @@
23.4 let
23.5 val ctxt = Proof.context_of state;
23.6 val prop = Syntax.read_prop ctxt s;
23.7 - in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
23.8 + in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
23.9
23.10 fun string_of_term state s =
23.11 let
23.12 @@ -571,15 +571,15 @@
23.13 val T = Term.type_of t;
23.14 in
23.15 Pretty.string_of
23.16 - (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
23.17 - Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
23.18 + (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
23.19 + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
23.20 end;
23.21
23.22 fun string_of_type state s =
23.23 let
23.24 val ctxt = Proof.context_of state;
23.25 val T = ProofContext.read_typ ctxt s;
23.26 - in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
23.27 + in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
23.28
23.29 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
23.30 PrintMode.with_modes modes (fn () =>
24.1 --- a/src/Pure/Isar/locale.ML Mon Oct 08 22:06:32 2007 +0200
24.2 +++ b/src/Pure/Isar/locale.ML Tue Oct 09 00:20:13 2007 +0200
24.3 @@ -472,7 +472,7 @@
24.4 fun print_registrations show_wits loc ctxt =
24.5 let
24.6 val thy = ProofContext.theory_of ctxt;
24.7 - val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
24.8 + val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
24.9 val prt_thm = prt_term o prop_of;
24.10 fun prt_inst ts =
24.11 Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
24.12 @@ -1545,7 +1545,7 @@
24.13 | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
24.14 handle Termtab.DUP t =>
24.15 error ("Conflicting interpreting equations for term " ^
24.16 - quote (ProofContext.string_of_term ctxt t))
24.17 + quote (Syntax.string_of_term ctxt t))
24.18 in ((id', eqns'), eqns') end;
24.19
24.20
25.1 --- a/src/Pure/Isar/obtain.ML Mon Oct 08 22:06:32 2007 +0200
25.2 +++ b/src/Pure/Isar/obtain.ML Tue Oct 09 00:20:13 2007 +0200
25.3 @@ -71,7 +71,7 @@
25.4 if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
25.5 val _ = null bads orelse
25.6 error ("Result contains obtained parameters: " ^
25.7 - space_implode " " (map (ProofContext.string_of_term ctxt) bads));
25.8 + space_implode " " (map (Syntax.string_of_term ctxt) bads));
25.9 in tm end;
25.10
25.11 fun eliminate fix_ctxt rule xs As thm =
25.12 @@ -217,8 +217,8 @@
25.13 val thy = ProofContext.theory_of ctxt;
25.14 val certT = Thm.ctyp_of thy;
25.15 val cert = Thm.cterm_of thy;
25.16 - val string_of_typ = ProofContext.string_of_typ ctxt;
25.17 - val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
25.18 + val string_of_typ = Syntax.string_of_typ ctxt;
25.19 + val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
25.20
25.21 fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
25.22
26.1 --- a/src/Pure/Isar/proof.ML Mon Oct 08 22:06:32 2007 +0200
26.2 +++ b/src/Pure/Isar/proof.ML Tue Oct 09 00:20:13 2007 +0200
26.3 @@ -465,7 +465,7 @@
26.4 let
26.5 val thy = theory_of state;
26.6 val ctxt = context_of state;
26.7 - val string_of_term = ProofContext.string_of_term ctxt;
26.8 + val string_of_term = Syntax.string_of_term ctxt;
26.9 val string_of_thm = ProofContext.string_of_thm ctxt;
26.10
26.11 val ngoals = Thm.nprems_of goal;
27.1 --- a/src/Pure/Isar/proof_display.ML Mon Oct 08 22:06:32 2007 +0200
27.2 +++ b/src/Pure/Isar/proof_display.ML Tue Oct 09 00:20:13 2007 +0200
27.3 @@ -43,8 +43,8 @@
27.4
27.5 fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
27.6
27.7 -val pprint_typ = pprint ProofContext.pretty_typ;
27.8 -val pprint_term = pprint ProofContext.pretty_term;
27.9 +val pprint_typ = pprint Syntax.pretty_typ;
27.10 +val pprint_term = pprint Syntax.pretty_term;
27.11 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
27.12 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
27.13 val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
27.14 @@ -136,7 +136,7 @@
27.15
27.16 fun pretty_var ctxt (x, T) =
27.17 Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
27.18 - Pretty.quote (ProofContext.pretty_typ ctxt T)];
27.19 + Pretty.quote (Syntax.pretty_typ ctxt T)];
27.20
27.21 fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
27.22
28.1 --- a/src/Pure/Isar/toplevel.ML Mon Oct 08 22:06:32 2007 +0200
28.2 +++ b/src/Pure/Isar/toplevel.ML Tue Oct 09 00:20:13 2007 +0200
28.3 @@ -273,10 +273,10 @@
28.4 raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
28.5 | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
28.6 | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
28.7 - with_context ProofContext.string_of_typ Ts @ with_context ProofContext.string_of_term ts)
28.8 + with_context Syntax.string_of_typ Ts @ with_context Syntax.string_of_term ts)
28.9 | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
28.10 | exn_msg true (TERM (msg, ts)) =
28.11 - raised "TERM" (msg :: with_context ProofContext.string_of_term ts)
28.12 + raised "TERM" (msg :: with_context Syntax.string_of_term ts)
28.13 | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
28.14 | exn_msg true (THM (msg, i, thms)) =
28.15 raised ("THM " ^ string_of_int i) (msg :: with_context ProofContext.string_of_thm thms)
29.1 --- a/src/Pure/Thy/term_style.ML Mon Oct 08 22:06:32 2007 +0200
29.2 +++ b/src/Pure/Thy/term_style.ML Tue Oct 09 00:20:13 2007 +0200
29.3 @@ -55,14 +55,14 @@
29.4 (Logic.strip_imp_concl t)
29.5 in
29.6 case concl of (_ $ l $ r) => (l, r)
29.7 - | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
29.8 + | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
29.9 end;
29.10
29.11 fun style_parm_premise i ctxt t =
29.12 let val prems = Logic.strip_imp_prems t in
29.13 if i <= length prems then nth prems (i - 1)
29.14 else error ("Not enough premises for prem" ^ string_of_int i ^
29.15 - " in propositon: " ^ ProofContext.string_of_term ctxt t)
29.16 + " in propositon: " ^ Syntax.string_of_term ctxt t)
29.17 end;
29.18
29.19 val _ = Context.add_setup
30.1 --- a/src/Pure/Thy/thy_output.ML Mon Oct 08 22:06:32 2007 +0200
30.2 +++ b/src/Pure/Thy/thy_output.ML Tue Oct 09 00:20:13 2007 +0200
30.3 @@ -429,22 +429,23 @@
30.4
30.5 val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
30.6
30.7 -fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
30.8 +fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
30.9 +
30.10 fun pretty_term_abbrev ctxt =
30.11 ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
30.12
30.13 fun pretty_term_typ ctxt t =
30.14 - ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
30.15 + Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
30.16
30.17 -fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
30.18 +fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
30.19
30.20 fun pretty_term_const ctxt t =
30.21 if Term.is_Const t then pretty_term ctxt t
30.22 - else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
30.23 + else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
30.24
30.25 fun pretty_abbrev ctxt t =
30.26 let
30.27 - fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
30.28 + fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
30.29 val (head, args) = Term.strip_comb t;
30.30 val (c, T) = Term.dest_Const head handle TERM _ => err ();
30.31 val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
30.32 @@ -519,7 +520,7 @@
30.33 ("typeof", args Args.term (output pretty_term_typeof)),
30.34 ("const", args Args.term (output pretty_term_const)),
30.35 ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
30.36 - ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
30.37 + ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
30.38 ("text", args (Scan.lift Args.name) (output (K pretty_text))),
30.39 ("goals", output_goals true),
30.40 ("subgoals", output_goals false),
31.1 --- a/src/Pure/axclass.ML Mon Oct 08 22:06:32 2007 +0200
31.2 +++ b/src/Pure/axclass.ML Tue Oct 09 00:20:13 2007 +0200
31.3 @@ -148,7 +148,8 @@
31.4 fun the_classrel thy (c1, c2) =
31.5 (case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
31.6 SOME th => Thm.transfer thy th
31.7 - | NONE => error ("Unproven class relation " ^ Sign.string_of_classrel thy [c1, c2]));
31.8 + | NONE => error ("Unproven class relation " ^
31.9 + Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
31.10
31.11 fun put_classrel arg = map_instances (fn (classrel, arities) =>
31.12 (insert (eq_fst op =) arg classrel, arities));
31.13 @@ -157,7 +158,8 @@
31.14 fun the_arity thy a (c, Ss) =
31.15 (case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
31.16 SOME th => Thm.transfer thy th
31.17 - | NONE => error ("Unproven type arity " ^ Sign.string_of_arity thy (a, Ss, [c])));
31.18 + | NONE => error ("Unproven type arity " ^
31.19 + Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
31.20
31.21 fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
31.22 (classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
31.23 @@ -173,7 +175,7 @@
31.24 fun pretty_axclass (class, AxClass {def, intro, axioms, params}) =
31.25 Pretty.block (Pretty.fbreaks
31.26 [Pretty.block
31.27 - [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
31.28 + [Pretty.str "class ", Syntax.pretty_sort ctxt [class], Pretty.str ":"],
31.29 Pretty.strs ("parameters:" :: params_of thy class),
31.30 ProofContext.pretty_fact ctxt ("def", [def]),
31.31 ProofContext.pretty_fact ctxt (introN, [intro]),
31.32 @@ -233,11 +235,12 @@
31.33
31.34 fun prove_classrel raw_rel tac thy =
31.35 let
31.36 + val ctxt = ProofContext.init thy;
31.37 val (c1, c2) = cert_classrel thy raw_rel;
31.38 - val th = Goal.prove (ProofContext.init thy) [] []
31.39 + val th = Goal.prove ctxt [] []
31.40 (Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
31.41 cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
31.42 - quote (Sign.string_of_classrel thy [c1, c2]));
31.43 + quote (Syntax.string_of_classrel ctxt [c1, c2]));
31.44 in
31.45 thy
31.46 |> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
31.47 @@ -246,13 +249,14 @@
31.48
31.49 fun prove_arity raw_arity tac thy =
31.50 let
31.51 + val ctxt = ProofContext.init thy;
31.52 val arity = Sign.cert_arity thy raw_arity;
31.53 val names = map (prefix arity_prefix) (Logic.name_arities arity);
31.54 val props = Logic.mk_arities arity;
31.55 - val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
31.56 + val ths = Goal.prove_multi ctxt [] [] props
31.57 (fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
31.58 cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
31.59 - quote (Sign.string_of_arity thy arity));
31.60 + quote (Syntax.string_of_arity ctxt arity));
31.61 in
31.62 thy
31.63 |> PureThy.add_thms (map (rpair []) (names ~~ ths))
32.1 --- a/src/Pure/codegen.ML Mon Oct 08 22:06:32 2007 +0200
32.2 +++ b/src/Pure/codegen.ML Tue Oct 09 00:20:13 2007 +0200
32.3 @@ -982,8 +982,7 @@
32.4 | pretty_counterex ctxt (SOME cex) =
32.5 Pretty.chunks (Pretty.str "Counterexample found:\n" ::
32.6 map (fn (s, t) =>
32.7 - Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
32.8 - ProofContext.pretty_term ctxt t]) cex);
32.9 + Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
32.10
32.11 val auto_quickcheck = ref true;
32.12 val auto_quickcheck_time_limit = ref 5000;
32.13 @@ -1043,8 +1042,8 @@
32.14 val T = Term.type_of t;
32.15 in
32.16 Pretty.writeln
32.17 - (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
32.18 - Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
32.19 + (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
32.20 + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
32.21 end);
32.22
32.23 exception Evaluation of term;
33.1 --- a/src/Pure/display.ML Mon Oct 08 22:06:32 2007 +0200
33.2 +++ b/src/Pure/display.ML Tue Oct 09 00:20:13 2007 +0200
33.3 @@ -146,12 +146,14 @@
33.4
33.5 fun pretty_full_theory verbose thy =
33.6 let
33.7 - fun prt_cls c = Sign.pretty_sort thy [c];
33.8 - fun prt_sort S = Sign.pretty_sort thy S;
33.9 - fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
33.10 - fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
33.11 + val ctxt = ProofContext.init thy;
33.12 +
33.13 + fun prt_cls c = Syntax.pretty_sort ctxt [c];
33.14 + fun prt_sort S = Syntax.pretty_sort ctxt S;
33.15 + fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
33.16 + fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
33.17 val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
33.18 - fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
33.19 + fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
33.20 val prt_term_no_vars = prt_term o Logic.unvarify;
33.21 fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
33.22 val prt_const' = Defs.pretty_const (Sign.pp thy);
34.1 --- a/src/Tools/induct.ML Mon Oct 08 22:06:32 2007 +0200
34.2 +++ b/src/Tools/induct.ML Tue Oct 09 00:20:13 2007 +0200
34.3 @@ -718,7 +718,7 @@
34.4 inst >> Option.map (pair NONE);
34.5
34.6 val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
34.7 - error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
34.8 + error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
34.9
34.10 fun unless_more_args scan = Scan.unless (Scan.lift
34.11 ((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
35.1 --- a/src/Tools/nbe.ML Mon Oct 08 22:06:32 2007 +0200
35.2 +++ b/src/Tools/nbe.ML Tue Oct 09 00:20:13 2007 +0200
35.3 @@ -393,8 +393,8 @@
35.4 val t' = norm_term thy t;
35.5 val ty' = Term.type_of t';
35.6 val p = PrintMode.with_modes modes (fn () =>
35.7 - Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
35.8 - Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty')]) ();
35.9 + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'), Pretty.fbrk,
35.10 + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')]) ();
35.11 in Pretty.writeln p end;
35.12
35.13