generic Syntax.pretty/string_of operations;
authorwenzelm
Tue Oct 09 00:20:13 2007 +0200 (2007-10-09)
changeset 249202a45e400fdad
parent 24919 ad3a8569759c
child 24921 708b2f887a42
generic Syntax.pretty/string_of operations;
NEWS
doc-src/antiquote_setup.ML
src/HOL/Algebra/ringsimp.ML
src/HOL/Library/Eval.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Orderings.thy
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/args.ML
src/Pure/Isar/class.ML
src/Pure/Isar/element.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/toplevel.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_output.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/display.ML
src/Tools/induct.ML
src/Tools/nbe.ML
     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