merged
authorwenzelm
Mon Apr 18 15:02:50 2011 +0200 (2011-04-18)
changeset 4239577eedb527068
parent 42393 c9bf3f8a8930
parent 42394 c65c07d9967a
child 42396 0869ce2006eb
merged
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 18 12:12:42 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 18 15:02:50 2011 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4      val tyvars = map (map (fn s =>
     1.5        (s, the (AList.lookup (op =) sorts s))) o #1) dts';
     1.6  
     1.7 -    fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
     1.8 +    fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
     1.9      fun augment_sort_typ thy S =
    1.10        let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
    1.11        in map_type_tfree (fn (s, S') => TFree (s,
     2.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 12:12:42 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 15:02:50 2011 +0200
     2.3 @@ -125,7 +125,7 @@
     2.4      val thy = Proof_Context.theory_of ctxt;
     2.5      val T = domain_type (fastype_of t);
     2.6      val T' = fastype_of u;
     2.7 -    val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
     2.8 +    val subst = Sign.typ_match thy (T, T') Vartab.empty
     2.9        handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
    2.10    in
    2.11      map_types (Envir.norm_type subst) t $ u
     3.1 --- a/src/HOL/Tools/enriched_type.ML	Mon Apr 18 12:12:42 2011 +0200
     3.2 +++ b/src/HOL/Tools/enriched_type.ML	Mon Apr 18 15:02:50 2011 +0200
     3.3 @@ -218,10 +218,11 @@
     3.4      val qualify = Binding.qualify true prfx o Binding.name;
     3.5      fun mapper_declaration comp_thm id_thm phi context =
     3.6        let
     3.7 -        val typ_instance = Type.typ_instance (Proof_Context.tsig_of (Context.proof_of context));
     3.8 +        val typ_instance = Sign.typ_instance (Context.theory_of context);
     3.9          val mapper' = Morphism.term phi mapper;
    3.10          val T_T' = pairself fastype_of (mapper, mapper');
    3.11 -      in if typ_instance T_T' andalso typ_instance (swap T_T')
    3.12 +      in
    3.13 +        if typ_instance T_T' andalso typ_instance (swap T_T')
    3.14          then (Data.map o Symtab.cons_list) (tyco,
    3.15            { mapper = mapper', variances = variances,
    3.16              comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
     4.1 --- a/src/Pure/General/pretty.ML	Mon Apr 18 12:12:42 2011 +0200
     4.2 +++ b/src/Pure/General/pretty.ML	Mon Apr 18 15:02:50 2011 +0200
     4.3 @@ -64,18 +64,6 @@
     4.4    val writeln: T -> unit
     4.5    val to_ML: T -> ML_Pretty.pretty
     4.6    val from_ML: ML_Pretty.pretty -> T
     4.7 -  type pp
     4.8 -  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
     4.9 -  val term: pp -> term -> T
    4.10 -  val typ: pp -> typ -> T
    4.11 -  val sort: pp -> sort -> T
    4.12 -  val classrel: pp -> class list -> T
    4.13 -  val arity: pp -> arity -> T
    4.14 -  val string_of_term: pp -> term -> string
    4.15 -  val string_of_typ: pp -> typ -> string
    4.16 -  val string_of_sort: pp -> sort -> string
    4.17 -  val string_of_classrel: pp -> class list -> string
    4.18 -  val string_of_arity: pp -> arity -> string
    4.19  end;
    4.20  
    4.21  structure Pretty: PRETTY =
    4.22 @@ -332,27 +320,4 @@
    4.23  
    4.24  end;
    4.25  
    4.26 -
    4.27 -
    4.28 -(** abstract pretty printing context **)
    4.29 -
    4.30 -datatype pp =
    4.31 -  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
    4.32 -
    4.33 -val pp = PP;
    4.34 -
    4.35 -fun pp_fun f (PP x) = f x;
    4.36 -
    4.37 -val term     = pp_fun #1;
    4.38 -val typ      = pp_fun #2;
    4.39 -val sort     = pp_fun #3;
    4.40 -val classrel = pp_fun #4;
    4.41 -val arity    = pp_fun #5;
    4.42 -
    4.43 -val string_of_term     = string_of oo term;
    4.44 -val string_of_typ      = string_of oo typ;
    4.45 -val string_of_sort     = string_of oo sort;
    4.46 -val string_of_classrel = string_of oo classrel;
    4.47 -val string_of_arity    = string_of oo arity;
    4.48 -
    4.49  end;
     5.1 --- a/src/Pure/Isar/class.ML	Mon Apr 18 12:12:42 2011 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Mon Apr 18 15:02:50 2011 +0200
     5.3 @@ -450,15 +450,16 @@
     5.4              (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
     5.5    end;
     5.6  
     5.7 -fun resort_terms pp algebra consts constraints ts =
     5.8 +fun resort_terms ctxt algebra consts constraints ts =
     5.9    let
    5.10 -    fun matchings (Const (c_ty as (c, _))) = (case constraints c
    5.11 -         of NONE => I
    5.12 -          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
    5.13 -              (Consts.typargs consts c_ty) sorts)
    5.14 -      | matchings _ = I
    5.15 +    fun matchings (Const (c_ty as (c, _))) =
    5.16 +          (case constraints c of
    5.17 +            NONE => I
    5.18 +          | SOME sorts =>
    5.19 +              fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
    5.20 +      | matchings _ = I;
    5.21      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
    5.22 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
    5.23 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
    5.24      val inst = map_type_tvar
    5.25        (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
    5.26    in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
    5.27 @@ -529,19 +530,20 @@
    5.28      val primary_constraints = map (apsnd
    5.29        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
    5.30      val algebra = Sign.classes_of thy
    5.31 -      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
    5.32 +      |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
    5.33              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    5.34      val consts = Sign.consts_of thy;
    5.35      val improve_constraints = AList.lookup (op =)
    5.36        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
    5.37 -    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
    5.38 -     of NONE => NONE
    5.39 -      | SOME ts' => SOME (ts', ctxt);
    5.40 +    fun resort_check ts ctxt =
    5.41 +      (case resort_terms ctxt algebra consts improve_constraints ts of
    5.42 +        NONE => NONE
    5.43 +      | SOME ts' => SOME (ts', ctxt));
    5.44      val lookup_inst_param = AxClass.lookup_inst_param consts params;
    5.45 -    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
    5.46 -    fun improve (c, ty) = case lookup_inst_param (c, ty)
    5.47 -     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
    5.48 -      | NONE => NONE;
    5.49 +    fun improve (c, ty) =
    5.50 +      (case lookup_inst_param (c, ty) of
    5.51 +        SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
    5.52 +      | NONE => NONE);
    5.53    in
    5.54      thy
    5.55      |> Theory.checkpoint
    5.56 @@ -559,7 +561,8 @@
    5.57          notes = Generic_Target.notes
    5.58            (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
    5.59          abbrev = Generic_Target.abbrev
    5.60 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
    5.61 +          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
    5.62 +            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    5.63          declaration = K Generic_Target.theory_declaration,
    5.64          syntax_declaration = K Generic_Target.theory_declaration,
    5.65          pretty = pretty,
     6.1 --- a/src/Pure/Isar/overloading.ML	Mon Apr 18 12:12:42 2011 +0200
     6.2 +++ b/src/Pure/Isar/overloading.ML	Mon Apr 18 15:02:50 2011 +0200
     6.3 @@ -63,20 +63,25 @@
     6.4  
     6.5  fun improve_term_check ts ctxt =
     6.6    let
     6.7 +    val thy = Proof_Context.theory_of ctxt;
     6.8 +
     6.9      val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
    6.10        ImprovableSyntax.get ctxt;
    6.11 -    val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
    6.12      val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
    6.13      val passed_or_abbrev = passed orelse is_abbrev;
    6.14 -    fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
    6.15 -         of SOME ty_ty' => Type.typ_match tsig ty_ty'
    6.16 +    fun accumulate_improvements (Const (c, ty)) =
    6.17 +          (case improve (c, ty) of
    6.18 +            SOME ty_ty' => Sign.typ_match thy ty_ty'
    6.19            | _ => I)
    6.20        | accumulate_improvements _ = I;
    6.21      val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
    6.22      val ts' = (map o map_types) (Envir.subst_type improvements) ts;
    6.23 -    fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
    6.24 -         of SOME (ty', t') =>
    6.25 -              if Type.typ_instance tsig (ty, ty')
    6.26 +    fun apply_subst t =
    6.27 +      Envir.expand_term
    6.28 +        (fn Const (c, ty) =>
    6.29 +          (case subst (c, ty) of
    6.30 +            SOME (ty', t') =>
    6.31 +              if Sign.typ_instance thy (ty, ty')
    6.32                then SOME (ty', apply_subst t') else NONE
    6.33            | NONE => NONE)
    6.34          | _ => NONE) t;
     7.1 --- a/src/Pure/Isar/proof_context.ML	Mon Apr 18 12:12:42 2011 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 15:02:50 2011 +0200
     7.3 @@ -302,7 +302,7 @@
     7.4    map_tsig (fn tsig as (local_tsig, global_tsig) =>
     7.5      let val thy_tsig = Sign.tsig_of thy in
     7.6        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
     7.7 -      else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
     7.8 +      else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
     7.9      end) |>
    7.10    map_consts (fn consts as (local_consts, global_consts) =>
    7.11      let val thy_consts = Sign.consts_of thy in
    7.12 @@ -376,7 +376,7 @@
    7.13  
    7.14  fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
    7.15    let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
    7.16 -  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
    7.17 +  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
    7.18  
    7.19  in
    7.20  
    7.21 @@ -546,7 +546,7 @@
    7.22  
    7.23  local
    7.24  
    7.25 -fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
    7.26 +fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
    7.27    (not (abbrev_mode ctxt)) (consts_of ctxt);
    7.28  
    7.29  fun expand_binds ctxt =
    7.30 @@ -666,9 +666,9 @@
    7.31  fun gen_cert prop ctxt t =
    7.32    t
    7.33    |> expand_abbrevs ctxt
    7.34 -  |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    7.35 -    handle TYPE (msg, _, _) => error msg
    7.36 -      | TERM (msg, _) => error msg);
    7.37 +  |> (fn t' =>
    7.38 +      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    7.39 +        handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
    7.40  
    7.41  in
    7.42  
     8.1 --- a/src/Pure/ROOT.ML	Mon Apr 18 12:12:42 2011 +0200
     8.2 +++ b/src/Pure/ROOT.ML	Mon Apr 18 15:02:50 2011 +0200
     8.3 @@ -53,6 +53,7 @@
     8.4  use "General/xml.ML";
     8.5  use "General/xml_data.ML";
     8.6  use "General/yxml.ML";
     8.7 +use "General/pretty.ML";
     8.8  
     8.9  use "General/sha1.ML";
    8.10  if String.isPrefix "polyml" ml_system
    8.11 @@ -103,24 +104,15 @@
    8.12  
    8.13  use "name.ML";
    8.14  use "term.ML";
    8.15 -use "term_ord.ML";
    8.16 -use "term_subst.ML";
    8.17 -use "old_term.ML";
    8.18 -use "General/pretty.ML";
    8.19  use "context.ML";
    8.20  use "config.ML";
    8.21  use "context_position.ML";
    8.22 -use "General/name_space.ML";
    8.23 -use "sorts.ML";
    8.24 -use "type.ML";
    8.25 -use "logic.ML";
    8.26  
    8.27  
    8.28  (* inner syntax *)
    8.29  
    8.30  use "Syntax/term_position.ML";
    8.31  use "Syntax/lexicon.ML";
    8.32 -use "Syntax/simple_syntax.ML";
    8.33  use "Syntax/ast.ML";
    8.34  use "Syntax/syntax_ext.ML";
    8.35  use "Syntax/parser.ML";
    8.36 @@ -132,6 +124,14 @@
    8.37  
    8.38  (* core of tactical proof system *)
    8.39  
    8.40 +use "term_ord.ML";
    8.41 +use "term_subst.ML";
    8.42 +use "old_term.ML";
    8.43 +use "General/name_space.ML";
    8.44 +use "sorts.ML";
    8.45 +use "type.ML";
    8.46 +use "logic.ML";
    8.47 +use "Syntax/simple_syntax.ML";
    8.48  use "net.ML";
    8.49  use "item_net.ML";
    8.50  use "envir.ML";
     9.1 --- a/src/Pure/Syntax/printer.ML	Mon Apr 18 12:12:42 2011 +0200
     9.2 +++ b/src/Pure/Syntax/printer.ML	Mon Apr 18 15:02:50 2011 +0200
     9.3 @@ -36,12 +36,12 @@
     9.4    val pretty_term_ast: bool -> Proof.context -> prtabs ->
     9.5      (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     9.6      (string -> string -> Pretty.T option) ->
     9.7 -    (string -> Markup.T list * xstring) ->
     9.8 +    (string -> Markup.T list * string) ->
     9.9      Ast.ast -> Pretty.T list
    9.10    val pretty_typ_ast: Proof.context -> prtabs ->
    9.11      (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
    9.12      (string -> string -> Pretty.T option) ->
    9.13 -    (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
    9.14 +    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
    9.15  end;
    9.16  
    9.17  structure Printer: PRINTER =
    10.1 --- a/src/Pure/Syntax/syntax.ML	Mon Apr 18 12:12:42 2011 +0200
    10.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 18 15:02:50 2011 +0200
    10.3 @@ -10,6 +10,8 @@
    10.4    val const: string -> term
    10.5    val free: string -> term
    10.6    val var: indexname -> term
    10.7 +  type operations
    10.8 +  val install_operations: operations -> unit
    10.9    val root: string Config.T
   10.10    val positions_raw: Config.raw
   10.11    val positions: bool Config.T
   10.12 @@ -28,14 +30,6 @@
   10.13    val unparse_arity: Proof.context -> arity -> Pretty.T
   10.14    val unparse_typ: Proof.context -> typ -> Pretty.T
   10.15    val unparse_term: Proof.context -> term -> Pretty.T
   10.16 -  val install_operations:
   10.17 -   {parse_sort: Proof.context -> string -> sort,
   10.18 -    parse_typ: Proof.context -> string -> typ,
   10.19 -    parse_term: Proof.context -> string -> term,
   10.20 -    parse_prop: Proof.context -> string -> term,
   10.21 -    unparse_sort: Proof.context -> sort -> Pretty.T,
   10.22 -    unparse_typ: Proof.context -> typ -> Pretty.T,
   10.23 -    unparse_term: Proof.context -> term -> Pretty.T} -> unit
   10.24    val print_checks: Proof.context -> unit
   10.25    val add_typ_check: int -> string ->
   10.26      (typ list -> Proof.context -> (typ list * Proof.context) option) ->
   10.27 @@ -49,6 +43,10 @@
   10.28    val add_term_uncheck: int -> string ->
   10.29      (term list -> Proof.context -> (term list * Proof.context) option) ->
   10.30      Context.generic -> Context.generic
   10.31 +  val typ_check: Proof.context -> typ list -> typ list
   10.32 +  val term_check: Proof.context -> term list -> term list
   10.33 +  val typ_uncheck: Proof.context -> typ list -> typ list
   10.34 +  val term_uncheck: Proof.context -> term list -> term list
   10.35    val check_sort: Proof.context -> sort -> sort
   10.36    val check_typ: Proof.context -> typ -> typ
   10.37    val check_term: Proof.context -> term -> term
   10.38 @@ -84,14 +82,13 @@
   10.39    val is_pretty_global: Proof.context -> bool
   10.40    val set_pretty_global: bool -> Proof.context -> Proof.context
   10.41    val init_pretty_global: theory -> Proof.context
   10.42 +  val init_pretty: Context.pretty -> Proof.context
   10.43    val pretty_term_global: theory -> term -> Pretty.T
   10.44    val pretty_typ_global: theory -> typ -> Pretty.T
   10.45    val pretty_sort_global: theory -> sort -> Pretty.T
   10.46    val string_of_term_global: theory -> term -> string
   10.47    val string_of_typ_global: theory -> typ -> string
   10.48    val string_of_sort_global: theory -> sort -> string
   10.49 -  val pp: Proof.context -> Pretty.pp
   10.50 -  val pp_global: theory -> Pretty.pp
   10.51    type syntax
   10.52    val eq_syntax: syntax * syntax -> bool
   10.53    val lookup_const: syntax -> string -> string option
   10.54 @@ -151,6 +148,31 @@
   10.55  
   10.56  (** inner syntax operations **)
   10.57  
   10.58 +(* back-patched operations *)
   10.59 +
   10.60 +type operations =
   10.61 + {parse_sort: Proof.context -> string -> sort,
   10.62 +  parse_typ: Proof.context -> string -> typ,
   10.63 +  parse_term: Proof.context -> string -> term,
   10.64 +  parse_prop: Proof.context -> string -> term,
   10.65 +  unparse_sort: Proof.context -> sort -> Pretty.T,
   10.66 +  unparse_typ: Proof.context -> typ -> Pretty.T,
   10.67 +  unparse_term: Proof.context -> term -> Pretty.T,
   10.68 +  check_typs: Proof.context -> typ list -> typ list,
   10.69 +  check_terms: Proof.context -> term list -> term list,
   10.70 +  check_props: Proof.context -> term list -> term list,
   10.71 +  uncheck_typs: Proof.context -> typ list -> typ list,
   10.72 +  uncheck_terms: Proof.context -> term list -> term list};
   10.73 +
   10.74 +val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
   10.75 +fun install_operations ops = Single_Assignment.assign operations ops;
   10.76 +
   10.77 +fun operation which ctxt x =
   10.78 +  (case Single_Assignment.peek operations of
   10.79 +    NONE => raise Fail "Inner syntax operations not installed"
   10.80 +  | SOME ops => which ops ctxt x);
   10.81 +
   10.82 +
   10.83  (* configuration options *)
   10.84  
   10.85  val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
   10.86 @@ -191,26 +213,6 @@
   10.87      val _ = Context_Position.report ctxt pos markup;
   10.88    in (syms, pos) end;
   10.89  
   10.90 -local
   10.91 -
   10.92 -type operations =
   10.93 - {parse_sort: Proof.context -> string -> sort,
   10.94 -  parse_typ: Proof.context -> string -> typ,
   10.95 -  parse_term: Proof.context -> string -> term,
   10.96 -  parse_prop: Proof.context -> string -> term,
   10.97 -  unparse_sort: Proof.context -> sort -> Pretty.T,
   10.98 -  unparse_typ: Proof.context -> typ -> Pretty.T,
   10.99 -  unparse_term: Proof.context -> term -> Pretty.T};
  10.100 -
  10.101 -val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
  10.102 -
  10.103 -fun operation which ctxt x =
  10.104 -  (case Single_Assignment.peek operations of
  10.105 -    NONE => raise Fail "Inner syntax operations not installed"
  10.106 -  | SOME ops => which ops ctxt x);
  10.107 -
  10.108 -in
  10.109 -
  10.110  val parse_sort = operation #parse_sort;
  10.111  val parse_typ = operation #parse_typ;
  10.112  val parse_term = operation #parse_term;
  10.113 @@ -219,10 +221,6 @@
  10.114  val unparse_typ = operation #unparse_typ;
  10.115  val unparse_term = operation #unparse_term;
  10.116  
  10.117 -fun install_operations ops = Single_Assignment.assign operations ops;
  10.118 -
  10.119 -end;
  10.120 -
  10.121  
  10.122  (* context-sensitive (un)checking *)
  10.123  
  10.124 @@ -290,17 +288,22 @@
  10.125  fun add_typ_uncheck stage = gen_add apfst (stage, true);
  10.126  fun add_term_uncheck stage = gen_add apsnd (stage, true);
  10.127  
  10.128 -val check_typs = gen_check fst false;
  10.129 -val check_terms = gen_check snd false;
  10.130 -fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
  10.131 +val typ_check = gen_check fst false;
  10.132 +val term_check = gen_check snd false;
  10.133 +val typ_uncheck = gen_check fst true;
  10.134 +val term_uncheck = gen_check snd true;
  10.135 +
  10.136 +val check_typs = operation #check_typs;
  10.137 +val check_terms = operation #check_terms;
  10.138 +val check_props = operation #check_props;
  10.139  
  10.140  val check_typ = singleton o check_typs;
  10.141  val check_term = singleton o check_terms;
  10.142  val check_prop = singleton o check_props;
  10.143  val check_sort = map_sort o check_typ;
  10.144  
  10.145 -val uncheck_typs = gen_check fst true;
  10.146 -val uncheck_terms = gen_check snd true;
  10.147 +val uncheck_typs = operation #uncheck_typs;
  10.148 +val uncheck_terms = operation #uncheck_terms;
  10.149  val uncheck_sort = map_sort o singleton o uncheck_typs;
  10.150  
  10.151  end;
  10.152 @@ -371,6 +374,7 @@
  10.153  fun is_pretty_global ctxt = Config.get ctxt pretty_global;
  10.154  val set_pretty_global = Config.put pretty_global;
  10.155  val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
  10.156 +val init_pretty = Context.pretty_context init_pretty_global;
  10.157  
  10.158  val pretty_term_global = pretty_term o init_pretty_global;
  10.159  val pretty_typ_global = pretty_typ o init_pretty_global;
  10.160 @@ -381,23 +385,6 @@
  10.161  val string_of_sort_global = string_of_sort o init_pretty_global;
  10.162  
  10.163  
  10.164 -(* pp operations -- deferred evaluation *)
  10.165 -
  10.166 -fun pp ctxt = Pretty.pp
  10.167 - (fn x => pretty_term ctxt x,
  10.168 -  fn x => pretty_typ ctxt x,
  10.169 -  fn x => pretty_sort ctxt x,
  10.170 -  fn x => pretty_classrel ctxt x,
  10.171 -  fn x => pretty_arity ctxt x);
  10.172 -
  10.173 -fun pp_global thy = Pretty.pp
  10.174 - (fn x => pretty_term_global thy x,
  10.175 -  fn x => pretty_typ_global thy x,
  10.176 -  fn x => pretty_sort_global thy x,
  10.177 -  fn x => pretty_classrel (init_pretty_global thy) x,
  10.178 -  fn x => pretty_arity (init_pretty_global thy) x);
  10.179 -
  10.180 -
  10.181  
  10.182  (** tables of translation functions **)
  10.183  
    11.1 --- a/src/Pure/Syntax/syntax_phases.ML	Mon Apr 18 12:12:42 2011 +0200
    11.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Apr 18 15:02:50 2011 +0200
    11.3 @@ -702,6 +702,17 @@
    11.4  
    11.5  
    11.6  
    11.7 +(** check/uncheck **)
    11.8 +
    11.9 +val check_typs = Syntax.typ_check;
   11.10 +val check_terms = Syntax.term_check;
   11.11 +fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
   11.12 +
   11.13 +val uncheck_typs = Syntax.typ_uncheck;
   11.14 +val uncheck_terms = Syntax.term_uncheck;
   11.15 +
   11.16 +
   11.17 +
   11.18  (** install operations **)
   11.19  
   11.20  val _ = Syntax.install_operations
   11.21 @@ -711,6 +722,11 @@
   11.22     parse_prop = parse_term true,
   11.23     unparse_sort = unparse_sort,
   11.24     unparse_typ = unparse_typ,
   11.25 -   unparse_term = unparse_term};
   11.26 +   unparse_term = unparse_term,
   11.27 +   check_typs = check_typs,
   11.28 +   check_terms = check_terms,
   11.29 +   check_props = check_props,
   11.30 +   uncheck_typs = uncheck_typs,
   11.31 +   uncheck_terms = uncheck_terms};
   11.32  
   11.33  end;
    12.1 --- a/src/Pure/axclass.ML	Mon Apr 18 12:12:42 2011 +0200
    12.2 +++ b/src/Pure/axclass.ML	Mon Apr 18 15:02:50 2011 +0200
    12.3 @@ -59,12 +59,12 @@
    12.4  
    12.5  type param = string * class;
    12.6  
    12.7 -fun add_param pp ((x, c): param) params =
    12.8 +fun add_param ctxt ((x, c): param) params =
    12.9    (case AList.lookup (op =) params x of
   12.10      NONE => (x, c) :: params
   12.11 -  | SOME c' => error ("Duplicate class parameter " ^ quote x ^
   12.12 -      " for " ^ Pretty.string_of_sort pp [c] ^
   12.13 -      (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
   12.14 +  | SOME c' =>
   12.15 +      error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^
   12.16 +        (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c'])));
   12.17  
   12.18  
   12.19  (* setup data *)
   12.20 @@ -104,10 +104,14 @@
   12.21          proven_arities = proven_arities2, inst_params = inst_params2,
   12.22          diff_classrels = diff_classrels2}) =
   12.23      let
   12.24 +      val ctxt = Syntax.init_pretty pp;
   12.25 +
   12.26        val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
   12.27        val params' =
   12.28          if null params1 then params2
   12.29 -        else fold_rev (fn p => if member (op =) params1 p then I else add_param pp p) params2 params1;
   12.30 +        else
   12.31 +          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
   12.32 +            params2 params1;
   12.33  
   12.34        (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
   12.35        val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
   12.36 @@ -590,7 +594,7 @@
   12.37        |> #2
   12.38        |> Sign.restore_naming facts_thy
   12.39        |> map_axclasses (Symtab.update (class, axclass))
   12.40 -      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
   12.41 +      |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params);
   12.42  
   12.43    in (class, result_thy) end;
   12.44  
    13.1 --- a/src/Pure/consts.ML	Mon Apr 18 12:12:42 2011 +0200
    13.2 +++ b/src/Pure/consts.ML	Mon Apr 18 15:02:50 2011 +0200
    13.3 @@ -26,7 +26,7 @@
    13.4    val intern_syntax: T -> xstring -> string
    13.5    val extern_syntax: Proof.context -> T -> string -> xstring
    13.6    val read_const: T -> string -> term
    13.7 -  val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    13.8 +  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    13.9    val typargs: T -> string * typ -> typ list
   13.10    val instance: T -> string * typ list -> typ
   13.11    val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
   13.12 @@ -156,7 +156,8 @@
   13.13  fun certify pp tsig do_expand consts =
   13.14    let
   13.15      fun err msg (c, T) =
   13.16 -      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
   13.17 +      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
   13.18 +        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
   13.19      val certT = Type.cert_typ tsig;
   13.20      fun cert tm =
   13.21        let
   13.22 @@ -269,7 +270,7 @@
   13.23  
   13.24  fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   13.25    let
   13.26 -    val pp = Syntax.pp ctxt;
   13.27 +    val pp = Context.pretty ctxt;
   13.28      val cert_term = certify pp tsig false consts;
   13.29      val expand_term = certify pp tsig true consts;
   13.30      val force_expand = mode = Print_Mode.internal;
    14.1 --- a/src/Pure/context.ML	Mon Apr 18 12:12:42 2011 +0200
    14.2 +++ b/src/Pure/context.ML	Mon Apr 18 15:02:50 2011 +0200
    14.3 @@ -28,6 +28,7 @@
    14.4  sig
    14.5    include BASIC_CONTEXT
    14.6    (*theory context*)
    14.7 +  type pretty
    14.8    val parents_of: theory -> theory list
    14.9    val ancestors_of: theory -> theory list
   14.10    val theory_name: theory -> string
   14.11 @@ -52,7 +53,7 @@
   14.12    val copy_thy: theory -> theory
   14.13    val checkpoint_thy: theory -> theory
   14.14    val finish_thy: theory -> theory
   14.15 -  val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
   14.16 +  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
   14.17    (*proof context*)
   14.18    val raw_transfer: theory -> Proof.context -> Proof.context
   14.19    (*generic context*)
   14.20 @@ -71,6 +72,10 @@
   14.21    val proof_map: (generic -> generic) -> Proof.context -> Proof.context
   14.22    val theory_of: generic -> theory  (*total*)
   14.23    val proof_of: generic -> Proof.context  (*total*)
   14.24 +  (*pretty printing context*)
   14.25 +  val pretty: Proof.context -> pretty
   14.26 +  val pretty_global: theory -> pretty
   14.27 +  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
   14.28    (*thread data*)
   14.29    val thread_data: unit -> generic option
   14.30    val the_thread_data: unit -> generic
   14.31 @@ -86,7 +91,7 @@
   14.32    structure Theory_Data:
   14.33    sig
   14.34      val declare: Object.T -> (Object.T -> Object.T) ->
   14.35 -      (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
   14.36 +      (pretty -> Object.T * Object.T -> Object.T) -> serial
   14.37      val get: serial -> (Object.T -> 'a) -> theory -> 'a
   14.38      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
   14.39    end
   14.40 @@ -110,12 +115,14 @@
   14.41  (*private copy avoids potential conflict of table exceptions*)
   14.42  structure Datatab = Table(type key = int val ord = int_ord);
   14.43  
   14.44 +datatype pretty = Pretty of Object.T;
   14.45 +
   14.46  local
   14.47  
   14.48  type kind =
   14.49   {empty: Object.T,
   14.50    extend: Object.T -> Object.T,
   14.51 -  merge: Pretty.pp -> Object.T * Object.T -> Object.T};
   14.52 +  merge: pretty -> Object.T * Object.T -> Object.T};
   14.53  
   14.54  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
   14.55  
   14.56 @@ -546,6 +553,16 @@
   14.57  val proof_of = cases Proof_Context.init_global I;
   14.58  
   14.59  
   14.60 +(* pretty printing context *)
   14.61 +
   14.62 +exception PRETTY of generic;
   14.63 +
   14.64 +val pretty = Pretty o PRETTY o Proof;
   14.65 +val pretty_global = Pretty o PRETTY o Theory;
   14.66 +
   14.67 +fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   14.68 +
   14.69 +
   14.70  
   14.71  (** thread data **)
   14.72  
   14.73 @@ -593,7 +610,7 @@
   14.74    type T
   14.75    val empty: T
   14.76    val extend: T -> T
   14.77 -  val merge: Pretty.pp -> T * T -> T
   14.78 +  val merge: Context.pretty -> T * T -> T
   14.79  end;
   14.80  
   14.81  signature THEORY_DATA_ARGS =
    15.1 --- a/src/Pure/defs.ML	Mon Apr 18 12:12:42 2011 +0200
    15.2 +++ b/src/Pure/defs.ML	Mon Apr 18 15:02:50 2011 +0200
    15.3 @@ -7,7 +7,7 @@
    15.4  
    15.5  signature DEFS =
    15.6  sig
    15.7 -  val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
    15.8 +  val pretty_const: Proof.context -> string * typ list -> Pretty.T
    15.9    val plain_args: typ list -> bool
   15.10    type T
   15.11    type spec =
   15.12 @@ -18,8 +18,8 @@
   15.13     {restricts: ((string * typ list) * string) list,
   15.14      reducts: ((string * typ list) * (string * typ list) list) list}
   15.15    val empty: T
   15.16 -  val merge: Pretty.pp -> T * T -> T
   15.17 -  val define: Pretty.pp -> bool -> string option -> string ->
   15.18 +  val merge: Proof.context -> T * T -> T
   15.19 +  val define: Proof.context -> bool -> string option -> string ->
   15.20      string * typ list -> (string * typ list) list -> T -> T
   15.21  end
   15.22  
   15.23 @@ -30,11 +30,11 @@
   15.24  
   15.25  type args = typ list;
   15.26  
   15.27 -fun pretty_const pp (c, args) =
   15.28 +fun pretty_const ctxt (c, args) =
   15.29    let
   15.30      val prt_args =
   15.31        if null args then []
   15.32 -      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
   15.33 +      else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
   15.34    in Pretty.block (Pretty.str c :: prt_args) end;
   15.35  
   15.36  fun plain_args args =
   15.37 @@ -118,27 +118,27 @@
   15.38  local
   15.39  
   15.40  val prt = Pretty.string_of oo pretty_const;
   15.41 -fun err pp (c, args) (d, Us) s1 s2 =
   15.42 -  error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
   15.43 +fun err ctxt (c, args) (d, Us) s1 s2 =
   15.44 +  error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
   15.45  
   15.46  fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   15.47    | contained _ _ = false;
   15.48  
   15.49 -fun acyclic pp (c, args) (d, Us) =
   15.50 +fun acyclic ctxt (c, args) (d, Us) =
   15.51    c <> d orelse
   15.52    exists (fn U => exists (contained U) args) Us orelse
   15.53    is_none (match_args (args, Us)) orelse
   15.54 -  err pp (c, args) (d, Us) "Circular" "";
   15.55 +  err ctxt (c, args) (d, Us) "Circular" "";
   15.56  
   15.57 -fun wellformed pp defs (c, args) (d, Us) =
   15.58 +fun wellformed ctxt defs (c, args) (d, Us) =
   15.59    forall is_TVar Us orelse
   15.60    (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
   15.61      SOME (Ts, description) =>
   15.62 -      err pp (c, args) (d, Us) "Malformed"
   15.63 -        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote description ^ ")")
   15.64 +      err ctxt (c, args) (d, Us) "Malformed"
   15.65 +        ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
   15.66    | NONE => true);
   15.67  
   15.68 -fun reduction pp defs const deps =
   15.69 +fun reduction ctxt defs const deps =
   15.70    let
   15.71      fun reduct Us (Ts, rhs) =
   15.72        (case match_args (Ts, Us) of
   15.73 @@ -151,17 +151,17 @@
   15.74        if forall (is_none o #1) reds then NONE
   15.75        else SOME (fold_rev
   15.76          (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   15.77 -    val _ = forall (acyclic pp const) (the_default deps deps');
   15.78 +    val _ = forall (acyclic ctxt const) (the_default deps deps');
   15.79    in deps' end;
   15.80  
   15.81  in
   15.82  
   15.83 -fun normalize pp =
   15.84 +fun normalize ctxt =
   15.85    let
   15.86      fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   15.87        let
   15.88          val reducts' = reducts |> map (fn (args, deps) =>
   15.89 -          (args, perhaps (reduction pp defs (c, args)) deps));
   15.90 +          (args, perhaps (reduction ctxt defs (c, args)) deps));
   15.91        in
   15.92          if reducts = reducts' then (changed, defs)
   15.93          else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
   15.94 @@ -171,38 +171,38 @@
   15.95          (true, defs') => norm_all defs'
   15.96        | (false, _) => defs);
   15.97      fun check defs (c, {reducts, ...}: def) =
   15.98 -      reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
   15.99 +      reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
  15.100    in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
  15.101  
  15.102 -fun dependencies pp (c, args) restr deps =
  15.103 +fun dependencies ctxt (c, args) restr deps =
  15.104    map_def c (fn (specs, restricts, reducts) =>
  15.105      let
  15.106        val restricts' = Library.merge (op =) (restricts, restr);
  15.107        val reducts' = insert (op =) (args, deps) reducts;
  15.108      in (specs, restricts', reducts') end)
  15.109 -  #> normalize pp;
  15.110 +  #> normalize ctxt;
  15.111  
  15.112  end;
  15.113  
  15.114  
  15.115  (* merge *)
  15.116  
  15.117 -fun merge pp (Defs defs1, Defs defs2) =
  15.118 +fun merge ctxt (Defs defs1, Defs defs2) =
  15.119    let
  15.120      fun add_deps (c, args) restr deps defs =
  15.121        if AList.defined (op =) (reducts_of defs c) args then defs
  15.122 -      else dependencies pp (c, args) restr deps defs;
  15.123 +      else dependencies ctxt (c, args) restr deps defs;
  15.124      fun add_def (c, {restricts, reducts, ...}: def) =
  15.125        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
  15.126    in
  15.127      Defs (Symtab.join join_specs (defs1, defs2)
  15.128 -      |> normalize pp |> Symtab.fold add_def defs2)
  15.129 +      |> normalize ctxt |> Symtab.fold add_def defs2)
  15.130    end;
  15.131  
  15.132  
  15.133  (* define *)
  15.134  
  15.135 -fun define pp unchecked def description (c, args) deps (Defs defs) =
  15.136 +fun define ctxt unchecked def description (c, args) deps (Defs defs) =
  15.137    let
  15.138      val restr =
  15.139        if plain_args args orelse
  15.140 @@ -211,6 +211,6 @@
  15.141      val spec =
  15.142        (serial (), {def = def, description = description, lhs = args, rhs = deps});
  15.143      val defs' = defs |> update_specs c spec;
  15.144 -  in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
  15.145 +  in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
  15.146  
  15.147  end;
    16.1 --- a/src/Pure/display.ML	Mon Apr 18 12:12:42 2011 +0200
    16.2 +++ b/src/Pure/display.ML	Mon Apr 18 15:02:50 2011 +0200
    16.3 @@ -143,7 +143,7 @@
    16.4      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
    16.5      val prt_term_no_vars = prt_term o Logic.unvarify_global;
    16.6      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    16.7 -    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
    16.8 +    val prt_const' = Defs.pretty_const ctxt;
    16.9  
   16.10      fun pretty_classrel (c, []) = prt_cls c
   16.11        | pretty_classrel (c, cs) = Pretty.block
    17.1 --- a/src/Pure/sign.ML	Mon Apr 18 12:12:42 2011 +0200
    17.2 +++ b/src/Pure/sign.ML	Mon Apr 18 15:02:50 2011 +0200
    17.3 @@ -61,7 +61,7 @@
    17.4    val certify_sort: theory -> sort -> sort
    17.5    val certify_typ: theory -> typ -> typ
    17.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
    17.7 -  val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
    17.8 +  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
    17.9    val certify_term: theory -> term -> term * typ * int
   17.10    val cert_term: theory -> term -> term
   17.11    val cert_prop: theory -> term -> term
   17.12 @@ -144,12 +144,13 @@
   17.13  
   17.14    fun merge pp (sign1, sign2) =
   17.15      let
   17.16 +      val ctxt = Syntax.init_pretty pp;
   17.17        val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   17.18        val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   17.19  
   17.20        val naming = Name_Space.default_naming;
   17.21        val syn = Syntax.merge_syntaxes syn1 syn2;
   17.22 -      val tsig = Type.merge_tsig pp (tsig1, tsig2);
   17.23 +      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
   17.24        val consts = Consts.merge (consts1, consts2);
   17.25      in make_sign (naming, syn, tsig, consts) end;
   17.26  );
   17.27 @@ -243,11 +244,11 @@
   17.28  (* certify wrt. type signature *)
   17.29  
   17.30  val arity_number = Type.arity_number o tsig_of;
   17.31 -fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
   17.32 +fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
   17.33  
   17.34 -val certify_class         = Type.cert_class o tsig_of;
   17.35 -val certify_sort          = Type.cert_sort o tsig_of;
   17.36 -val certify_typ           = Type.cert_typ o tsig_of;
   17.37 +val certify_class = Type.cert_class o tsig_of;
   17.38 +val certify_sort = Type.cert_sort o tsig_of;
   17.39 +val certify_typ = Type.cert_typ o tsig_of;
   17.40  fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of;
   17.41  
   17.42  
   17.43 @@ -262,7 +263,7 @@
   17.44          val xs = map Free bs;           (*we do not rename here*)
   17.45          val t' = subst_bounds (xs, t);
   17.46          val u' = subst_bounds (xs, u);
   17.47 -        val msg = Type.appl_error pp t' T u' U;
   17.48 +        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
   17.49        in raise TYPE (msg, [T, U], [t', u']) end;
   17.50  
   17.51      fun typ_of (_, Const (_, T)) = T
   17.52 @@ -301,10 +302,11 @@
   17.53      val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   17.54    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   17.55  
   17.56 -fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
   17.57 -fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
   17.58 +fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
   17.59 +fun cert_term_abbrev thy =
   17.60 +  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
   17.61  val cert_term = #1 oo certify_term;
   17.62 -fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
   17.63 +fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
   17.64  
   17.65  end;
   17.66  
   17.67 @@ -454,15 +456,19 @@
   17.68  (* primitive classes and arities *)
   17.69  
   17.70  fun primitive_class (bclass, classes) thy =
   17.71 -  thy |> map_sign (fn (naming, syn, tsig, consts) =>
   17.72 +  thy
   17.73 +  |> map_sign (fn (naming, syn, tsig, consts) =>
   17.74      let
   17.75        val ctxt = Syntax.init_pretty_global thy;
   17.76 -      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
   17.77 +      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
   17.78      in (naming, syn, tsig', consts) end)
   17.79    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   17.80  
   17.81 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
   17.82 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
   17.83 +fun primitive_classrel arg thy =
   17.84 +  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
   17.85 +
   17.86 +fun primitive_arity arg thy =
   17.87 +  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
   17.88  
   17.89  
   17.90  (* add translation functions *)
    18.1 --- a/src/Pure/sorts.ML	Mon Apr 18 12:12:42 2011 +0200
    18.2 +++ b/src/Pure/sorts.ML	Mon Apr 18 15:02:50 2011 +0200
    18.3 @@ -40,15 +40,15 @@
    18.4    val minimal_sorts: algebra -> sort list -> sort Ord_List.T
    18.5    val certify_class: algebra -> class -> class    (*exception TYPE*)
    18.6    val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
    18.7 -  val add_class: Pretty.pp -> class * class list -> algebra -> algebra
    18.8 -  val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
    18.9 -  val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
   18.10 +  val add_class: Proof.context -> class * class list -> algebra -> algebra
   18.11 +  val add_classrel: Proof.context -> class * class -> algebra -> algebra
   18.12 +  val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
   18.13    val empty_algebra: algebra
   18.14 -  val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
   18.15 -  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
   18.16 +  val merge_algebra: Proof.context -> algebra * algebra -> algebra
   18.17 +  val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
   18.18      -> algebra -> (sort -> sort) * algebra
   18.19    type class_error
   18.20 -  val class_error: Pretty.pp -> class_error -> string
   18.21 +  val class_error: Proof.context -> class_error -> string
   18.22    exception CLASS_ERROR of class_error
   18.23    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   18.24    val meet_sort: algebra -> typ * sort
   18.25 @@ -198,16 +198,16 @@
   18.26  
   18.27  fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
   18.28  
   18.29 -fun err_cyclic_classes pp css =
   18.30 +fun err_cyclic_classes ctxt css =
   18.31    error (cat_lines (map (fn cs =>
   18.32 -    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   18.33 +    "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
   18.34  
   18.35 -fun add_class pp (c, cs) = map_classes (fn classes =>
   18.36 +fun add_class ctxt (c, cs) = map_classes (fn classes =>
   18.37    let
   18.38      val classes' = classes |> Graph.new_node (c, serial ())
   18.39        handle Graph.DUP dup => err_dup_class dup;
   18.40      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
   18.41 -      handle Graph.CYCLES css => err_cyclic_classes pp css;
   18.42 +      handle Graph.CYCLES css => err_cyclic_classes ctxt css;
   18.43    in classes'' end);
   18.44  
   18.45  
   18.46 @@ -216,15 +216,14 @@
   18.47  local
   18.48  
   18.49  fun for_classes _ NONE = ""
   18.50 -  | for_classes pp (SOME (c1, c2)) =
   18.51 -      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
   18.52 +  | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
   18.53  
   18.54 -fun err_conflict pp t cc (c, Ss) (c', Ss') =
   18.55 -  error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
   18.56 -    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
   18.57 -    Pretty.string_of_arity pp (t, Ss', [c']));
   18.58 +fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
   18.59 +  error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
   18.60 +    Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
   18.61 +    Syntax.string_of_arity ctxt (t, Ss', [c']));
   18.62  
   18.63 -fun coregular pp algebra t (c, Ss) ars =
   18.64 +fun coregular ctxt algebra t (c, Ss) ars =
   18.65    let
   18.66      fun conflict (c', Ss') =
   18.67        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
   18.68 @@ -234,62 +233,62 @@
   18.69        else NONE;
   18.70    in
   18.71      (case get_first conflict ars of
   18.72 -      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
   18.73 +      SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
   18.74      | NONE => (c, Ss) :: ars)
   18.75    end;
   18.76  
   18.77  fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
   18.78  
   18.79 -fun insert pp algebra t (c, Ss) ars =
   18.80 +fun insert ctxt algebra t (c, Ss) ars =
   18.81    (case AList.lookup (op =) ars c of
   18.82 -    NONE => coregular pp algebra t (c, Ss) ars
   18.83 +    NONE => coregular ctxt algebra t (c, Ss) ars
   18.84    | SOME Ss' =>
   18.85        if sorts_le algebra (Ss, Ss') then ars
   18.86        else if sorts_le algebra (Ss', Ss)
   18.87 -      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
   18.88 -      else err_conflict pp t NONE (c, Ss) (c, Ss'));
   18.89 +      then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
   18.90 +      else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
   18.91  
   18.92  in
   18.93  
   18.94 -fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
   18.95 +fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
   18.96  
   18.97 -fun insert_complete_ars pp algebra (t, ars) arities =
   18.98 +fun insert_complete_ars ctxt algebra (t, ars) arities =
   18.99    let val ars' =
  18.100      Symtab.lookup_list arities t
  18.101 -    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
  18.102 +    |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
  18.103    in Symtab.update (t, ars') arities end;
  18.104  
  18.105 -fun add_arities pp arg algebra =
  18.106 -  algebra |> map_arities (insert_complete_ars pp algebra arg);
  18.107 +fun add_arities ctxt arg algebra =
  18.108 +  algebra |> map_arities (insert_complete_ars ctxt algebra arg);
  18.109  
  18.110 -fun add_arities_table pp algebra =
  18.111 -  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
  18.112 +fun add_arities_table ctxt algebra =
  18.113 +  Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
  18.114  
  18.115  end;
  18.116  
  18.117  
  18.118  (* classrel *)
  18.119  
  18.120 -fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
  18.121 +fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
  18.122    Symtab.empty
  18.123 -  |> add_arities_table pp algebra arities);
  18.124 +  |> add_arities_table ctxt algebra arities);
  18.125  
  18.126 -fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
  18.127 +fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
  18.128    classes |> Graph.add_edge_trans_acyclic rel
  18.129 -    handle Graph.CYCLES css => err_cyclic_classes pp css);
  18.130 +    handle Graph.CYCLES css => err_cyclic_classes ctxt css);
  18.131  
  18.132  
  18.133  (* empty and merge *)
  18.134  
  18.135  val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
  18.136  
  18.137 -fun merge_algebra pp
  18.138 +fun merge_algebra ctxt
  18.139     (Algebra {classes = classes1, arities = arities1},
  18.140      Algebra {classes = classes2, arities = arities2}) =
  18.141    let
  18.142      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
  18.143        handle Graph.DUP c => err_dup_class c
  18.144 -        | Graph.CYCLES css => err_cyclic_classes pp css;
  18.145 +        | Graph.CYCLES css => err_cyclic_classes ctxt css;
  18.146      val algebra0 = make_algebra (classes', Symtab.empty);
  18.147      val arities' =
  18.148        (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
  18.149 @@ -297,20 +296,20 @@
  18.150        | (true, false) =>  (*no completion*)
  18.151            (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
  18.152              if pointer_eq (ars1, ars2) then raise Symtab.SAME
  18.153 -            else insert_ars pp algebra0 t ars2 ars1)
  18.154 +            else insert_ars ctxt algebra0 t ars2 ars1)
  18.155        | (false, true) =>  (*unary completion*)
  18.156            Symtab.empty
  18.157 -          |> add_arities_table pp algebra0 arities1
  18.158 +          |> add_arities_table ctxt algebra0 arities1
  18.159        | (false, false) => (*binary completion*)
  18.160            Symtab.empty
  18.161 -          |> add_arities_table pp algebra0 arities1
  18.162 -          |> add_arities_table pp algebra0 arities2);
  18.163 +          |> add_arities_table ctxt algebra0 arities1
  18.164 +          |> add_arities_table ctxt algebra0 arities2);
  18.165    in make_algebra (classes', arities') end;
  18.166  
  18.167  
  18.168  (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
  18.169  
  18.170 -fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
  18.171 +fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
  18.172    let
  18.173      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
  18.174      fun restrict_arity t (c, Ss) =
  18.175 @@ -322,7 +321,7 @@
  18.176        else NONE;
  18.177      val classes' = classes |> Graph.subgraph P;
  18.178      val arities' = arities |> Symtab.map (map_filter o restrict_arity);
  18.179 -  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
  18.180 +  in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
  18.181  
  18.182  
  18.183  
  18.184 @@ -335,13 +334,13 @@
  18.185    No_Arity of string * class |
  18.186    No_Subsort of sort * sort;
  18.187  
  18.188 -fun class_error pp (No_Classrel (c1, c2)) =
  18.189 -      "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
  18.190 -  | class_error pp (No_Arity (a, c)) =
  18.191 -      "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
  18.192 -  | class_error pp (No_Subsort (S1, S2)) =
  18.193 -     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
  18.194 -       ^ " < " ^ Pretty.string_of_sort pp S2;
  18.195 +fun class_error ctxt (No_Classrel (c1, c2)) =
  18.196 +      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
  18.197 +  | class_error ctxt (No_Arity (a, c)) =
  18.198 +      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
  18.199 +  | class_error ctxt (No_Subsort (S1, S2)) =
  18.200 +      "Cannot derive subsort relation " ^
  18.201 +        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
  18.202  
  18.203  exception CLASS_ERROR of class_error;
  18.204  
    19.1 --- a/src/Pure/theory.ML	Mon Apr 18 12:12:42 2011 +0200
    19.2 +++ b/src/Pure/theory.ML	Mon Apr 18 15:02:50 2011 +0200
    19.3 @@ -95,11 +95,12 @@
    19.4  
    19.5    fun merge pp (thy1, thy2) =
    19.6      let
    19.7 +      val ctxt = Syntax.init_pretty pp;
    19.8        val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
    19.9        val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   19.10  
   19.11        val axioms' = empty_axioms;
   19.12 -      val defs' = Defs.merge pp (defs1, defs2);
   19.13 +      val defs' = Defs.merge ctxt (defs1, defs2);
   19.14        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   19.15        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   19.16      in make_thy (axioms', defs', (bgs', ens')) end;
   19.17 @@ -137,7 +138,7 @@
   19.18  
   19.19  fun begin_theory name imports =
   19.20    let
   19.21 -    val thy = Context.begin_thy Syntax.pp_global name imports;
   19.22 +    val thy = Context.begin_thy Context.pretty_global name imports;
   19.23      val wrappers = begin_wrappers thy;
   19.24    in
   19.25      thy
   19.26 @@ -196,7 +197,7 @@
   19.27        else error ("Specification depends on extra type variables: " ^
   19.28          commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
   19.29          "\nThe error(s) above occurred in " ^ quote description);
   19.30 -  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
   19.31 +  in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
   19.32  
   19.33  fun add_deps ctxt a raw_lhs raw_rhs thy =
   19.34    let
   19.35 @@ -239,9 +240,8 @@
   19.36  
   19.37  local
   19.38  
   19.39 -fun check_def ctxt unchecked overloaded (b, tm) defs =
   19.40 +fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   19.41    let
   19.42 -    val thy = Proof_Context.theory_of ctxt;
   19.43      val name = Sign.full_name thy b;
   19.44      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   19.45        handle TERM (msg, _) => error msg;
   19.46 @@ -258,7 +258,7 @@
   19.47  fun add_def ctxt unchecked overloaded raw_axm thy =
   19.48    let val axm = cert_axm ctxt raw_axm in
   19.49      thy
   19.50 -    |> map_defs (check_def ctxt unchecked overloaded axm)
   19.51 +    |> map_defs (check_def ctxt thy unchecked overloaded axm)
   19.52      |> add_axiom ctxt axm
   19.53    end;
   19.54  
    20.1 --- a/src/Pure/type.ML	Mon Apr 18 12:12:42 2011 +0200
    20.2 +++ b/src/Pure/type.ML	Mon Apr 18 15:02:50 2011 +0200
    20.3 @@ -11,7 +11,7 @@
    20.4    val mark_polymorphic: typ -> typ
    20.5    val constraint: typ -> term -> term
    20.6    val strip_constraints: term -> term
    20.7 -  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
    20.8 +  val appl_error: Proof.context -> term -> typ -> term -> typ -> string
    20.9    (*type signatures and certified types*)
   20.10    datatype decl =
   20.11      LogicalType of int |
   20.12 @@ -55,7 +55,7 @@
   20.13    val cert_typ_mode: mode -> tsig -> typ -> typ
   20.14    val cert_typ: tsig -> typ -> typ
   20.15    val arity_number: tsig -> string -> int
   20.16 -  val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
   20.17 +  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
   20.18  
   20.19    (*special treatment of type vars*)
   20.20    val sort_of_atyp: typ -> sort
   20.21 @@ -86,17 +86,16 @@
   20.22    val eq_type: tyenv -> typ * typ -> bool
   20.23  
   20.24    (*extend and merge type signatures*)
   20.25 -  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
   20.26 -    binding * class list -> tsig -> tsig
   20.27 +  val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
   20.28    val hide_class: bool -> string -> tsig -> tsig
   20.29    val set_defsort: sort -> tsig -> tsig
   20.30    val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
   20.31    val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   20.32    val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   20.33    val hide_type: bool -> string -> tsig -> tsig
   20.34 -  val add_arity: Pretty.pp -> arity -> tsig -> tsig
   20.35 -  val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   20.36 -  val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
   20.37 +  val add_arity: Proof.context -> arity -> tsig -> tsig
   20.38 +  val add_classrel: Proof.context -> class * class -> tsig -> tsig
   20.39 +  val merge_tsig: Proof.context -> tsig * tsig -> tsig
   20.40  end;
   20.41  
   20.42  structure Type: TYPE =
   20.43 @@ -116,15 +115,15 @@
   20.44    | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
   20.45    | strip_constraints a = a;
   20.46  
   20.47 -fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
   20.48 +fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
   20.49        cat_lines
   20.50         ["Failed to meet type constraint:", "",
   20.51          Pretty.string_of (Pretty.block
   20.52 -         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
   20.53 -          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
   20.54 +         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u,
   20.55 +          Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]),
   20.56          Pretty.string_of (Pretty.block
   20.57 -         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
   20.58 -  | appl_error pp t T u U =
   20.59 +         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])]
   20.60 +  | appl_error ctxt t T u U =
   20.61        cat_lines
   20.62         ["Type error in application: " ^
   20.63            (case T of
   20.64 @@ -132,11 +131,11 @@
   20.65            | _ => "operator not of function type"),
   20.66          "",
   20.67          Pretty.string_of (Pretty.block
   20.68 -          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
   20.69 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
   20.70 +          [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t,
   20.71 +            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]),
   20.72          Pretty.string_of (Pretty.block
   20.73 -          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
   20.74 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
   20.75 +          [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u,
   20.76 +            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])];
   20.77  
   20.78  
   20.79  
   20.80 @@ -310,7 +309,7 @@
   20.81  
   20.82  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   20.83    | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
   20.84 -      handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
   20.85 +      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
   20.86  
   20.87  
   20.88  
   20.89 @@ -577,14 +576,14 @@
   20.90  
   20.91  (* classes *)
   20.92  
   20.93 -fun add_class ctxt pp naming (c, cs) tsig =
   20.94 +fun add_class ctxt naming (c, cs) tsig =
   20.95    tsig |> map_tsig (fn ((space, classes), default, types) =>
   20.96      let
   20.97        val cs' = map (cert_class tsig) cs
   20.98          handle TYPE (msg, _, _) => error msg;
   20.99        val _ = Binding.check c;
  20.100        val (c', space') = space |> Name_Space.declare ctxt true naming c;
  20.101 -      val classes' = classes |> Sorts.add_class pp (c', cs');
  20.102 +      val classes' = classes |> Sorts.add_class ctxt (c', cs');
  20.103      in ((space', classes'), default, types) end);
  20.104  
  20.105  fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
  20.106 @@ -593,7 +592,7 @@
  20.107  
  20.108  (* arities *)
  20.109  
  20.110 -fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
  20.111 +fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
  20.112    let
  20.113      val _ =
  20.114        (case lookup_type tsig t of
  20.115 @@ -602,18 +601,18 @@
  20.116        | NONE => error (undecl_type t));
  20.117      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
  20.118        handle TYPE (msg, _, _) => error msg;
  20.119 -    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
  20.120 +    val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
  20.121    in ((space, classes'), default, types) end);
  20.122  
  20.123  
  20.124  (* classrel *)
  20.125  
  20.126 -fun add_classrel pp rel tsig =
  20.127 +fun add_classrel ctxt rel tsig =
  20.128    tsig |> map_tsig (fn ((space, classes), default, types) =>
  20.129      let
  20.130        val rel' = pairself (cert_class tsig) rel
  20.131          handle TYPE (msg, _, _) => error msg;
  20.132 -      val classes' = classes |> Sorts.add_classrel pp rel';
  20.133 +      val classes' = classes |> Sorts.add_classrel ctxt rel';
  20.134      in ((space, classes'), default, types) end);
  20.135  
  20.136  
  20.137 @@ -674,7 +673,7 @@
  20.138  
  20.139  (* merge type signatures *)
  20.140  
  20.141 -fun merge_tsig pp (tsig1, tsig2) =
  20.142 +fun merge_tsig ctxt (tsig1, tsig2) =
  20.143    let
  20.144      val (TSig {classes = (space1, classes1), default = default1, types = types1,
  20.145        log_types = _}) = tsig1;
  20.146 @@ -682,7 +681,7 @@
  20.147        log_types = _}) = tsig2;
  20.148  
  20.149      val space' = Name_Space.merge (space1, space2);
  20.150 -    val classes' = Sorts.merge_algebra pp (classes1, classes2);
  20.151 +    val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
  20.152      val default' = Sorts.inter_sort classes' (default1, default2);
  20.153      val types' = Name_Space.merge_tables (types1, types2);
  20.154    in build_tsig ((space', classes'), default', types') end;
    21.1 --- a/src/Pure/type_infer.ML	Mon Apr 18 12:12:42 2011 +0200
    21.2 +++ b/src/Pure/type_infer.ML	Mon Apr 18 15:02:50 2011 +0200
    21.3 @@ -217,10 +217,10 @@
    21.4  
    21.5  exception NO_UNIFIER of string * typ Vartab.table;
    21.6  
    21.7 -fun unify ctxt pp =
    21.8 +fun unify ctxt =
    21.9    let
   21.10      val thy = Proof_Context.theory_of ctxt;
   21.11 -    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
   21.12 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   21.13  
   21.14  
   21.15      (* adjust sorts of parameters *)
   21.16 @@ -289,9 +289,6 @@
   21.17  
   21.18  fun infer ctxt =
   21.19    let
   21.20 -    val pp = Syntax.pp ctxt;
   21.21 -
   21.22 -
   21.23      (* errors *)
   21.24  
   21.25      fun prep_output tye bs ts Ts =
   21.26 @@ -310,7 +307,7 @@
   21.27  
   21.28      fun err_appl msg tye bs t T u U =
   21.29        let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   21.30 -      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
   21.31 +      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
   21.32  
   21.33  
   21.34      (* main *)
   21.35 @@ -328,7 +325,7 @@
   21.36              val (T, tye_idx') = inf bs t tye_idx;
   21.37              val (U, (tye, idx)) = inf bs u tye_idx';
   21.38              val V = mk_param idx [];
   21.39 -            val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
   21.40 +            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
   21.41                handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
   21.42            in (V, tye_idx'') end;
   21.43  
    22.1 --- a/src/Tools/Code/code_preproc.ML	Mon Apr 18 12:12:42 2011 +0200
    22.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 15:02:50 2011 +0200
    22.3 @@ -431,8 +431,7 @@
    22.4        |> fold (ensure_fun thy arities eqngr) cs
    22.5        |> fold (ensure_rhs thy arities eqngr) cs_rhss;
    22.6      val arities' = fold (add_arity thy vardeps) insts arities;
    22.7 -    val pp = Syntax.pp_global thy;
    22.8 -    val algebra = Sorts.subalgebra pp (is_proper_class thy)
    22.9 +    val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
   22.10        (AList.lookup (op =) arities') (Sign.classes_of thy);
   22.11      val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
   22.12      fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
    23.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 18 12:12:42 2011 +0200
    23.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 15:02:50 2011 +0200
    23.3 @@ -574,18 +574,25 @@
    23.4  fun translation_error thy permissive some_thm msg sub_msg =
    23.5    if permissive
    23.6    then raise PERMISSIVE ()
    23.7 -  else let
    23.8 -    val err_thm = case some_thm
    23.9 -     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
   23.10 -      | NONE => "";
   23.11 -  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
   23.12 +  else
   23.13 +    let
   23.14 +      val err_thm =
   23.15 +        (case some_thm of
   23.16 +          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
   23.17 +        | NONE => "");
   23.18 +    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
   23.19  
   23.20  fun not_wellsorted thy permissive some_thm ty sort e =
   23.21    let
   23.22 -    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
   23.23 -    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
   23.24 -      ^ Syntax.string_of_sort_global thy sort;
   23.25 -  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
   23.26 +    val ctxt = Syntax.init_pretty_global thy;
   23.27 +    val err_class = Sorts.class_error ctxt e;
   23.28 +    val err_typ =
   23.29 +      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
   23.30 +        Syntax.string_of_sort_global thy sort;
   23.31 +  in
   23.32 +    translation_error thy permissive some_thm "Wellsortedness error"
   23.33 +      (err_typ ^ "\n" ^ err_class)
   23.34 +  end;
   23.35  
   23.36  
   23.37  (* translation *)
    24.1 --- a/src/Tools/subtyping.ML	Mon Apr 18 12:12:42 2011 +0200
    24.2 +++ b/src/Tools/subtyping.ML	Mon Apr 18 15:02:50 2011 +0200
    24.3 @@ -98,8 +98,7 @@
    24.4  fun unify weak ctxt =
    24.5    let
    24.6      val thy = Proof_Context.theory_of ctxt;
    24.7 -    val pp = Syntax.pp ctxt;
    24.8 -    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
    24.9 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   24.10  
   24.11  
   24.12      (* adjust sorts of parameters *)
   24.13 @@ -190,8 +189,8 @@
   24.14  
   24.15  (** error messages **)
   24.16  
   24.17 -fun gen_msg err msg = 
   24.18 -  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
   24.19 +fun gen_msg err msg =
   24.20 +  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
   24.21    (if msg = "" then "" else ": " ^ msg) ^ "\n";
   24.22  
   24.23  fun prep_output ctxt tye bs ts Ts =
   24.24 @@ -204,27 +203,26 @@
   24.25    in (map prep ts', Ts') end;
   24.26  
   24.27  fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   24.28 -  
   24.29 +
   24.30  fun unif_failed msg =
   24.31    "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   24.32 -  
   24.33 +
   24.34  fun err_appl_msg ctxt msg tye bs t T u U () =
   24.35    let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
   24.36 -  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
   24.37 +  in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end;
   24.38  
   24.39  fun err_list ctxt msg tye Ts =
   24.40    let
   24.41      val (_, Ts') = prep_output ctxt tye [] [] Ts;
   24.42 -    val text = cat_lines ([msg,
   24.43 -      "Cannot unify a list of types that should be the same:",
   24.44 -      (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
   24.45 +    val text =
   24.46 +      msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^
   24.47 +        Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts'));
   24.48    in
   24.49      error text
   24.50    end;
   24.51  
   24.52  fun err_bound ctxt msg tye packs =
   24.53    let
   24.54 -    val pp = Syntax.pp ctxt;
   24.55      val (ts, Ts) = fold
   24.56        (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
   24.57          let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
   24.58 @@ -233,9 +231,10 @@
   24.59      val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
   24.60          (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
   24.61            Pretty.block [
   24.62 -            Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
   24.63 -            Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
   24.64 -            Pretty.block [Pretty.term pp (t $ u)]]))
   24.65 +            Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2,
   24.66 +            Syntax.pretty_typ ctxt U, Pretty.brk 3,
   24.67 +            Pretty.str "from function application", Pretty.brk 2,
   24.68 +            Pretty.block [Syntax.pretty_term ctxt (t $ u)]]))
   24.69          ts Ts))
   24.70    in
   24.71      error text
   24.72 @@ -277,21 +276,20 @@
   24.73  
   24.74  fun process_constraints ctxt err cs tye_idx =
   24.75    let
   24.76 +    val thy = Proof_Context.theory_of ctxt;
   24.77 +
   24.78      val coes_graph = coes_graph_of ctxt;
   24.79      val tmaps = tmaps_of ctxt;
   24.80 -    val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
   24.81 -    val pp = Syntax.pp ctxt;
   24.82 -    val arity_sorts = Type.arity_sorts pp tsig;
   24.83 -    val subsort = Type.subsort tsig;
   24.84 +    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
   24.85  
   24.86      fun split_cs _ [] = ([], [])
   24.87        | split_cs f (c :: cs) =
   24.88            (case pairself f (fst c) of
   24.89              (false, false) => apsnd (cons c) (split_cs f cs)
   24.90            | _ => apfst (cons c) (split_cs f cs));
   24.91 -          
   24.92 +
   24.93      fun unify_list (T :: Ts) tye_idx =
   24.94 -      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;      
   24.95 +      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
   24.96  
   24.97  
   24.98      (* check whether constraint simplification will terminate using weak unification *)
   24.99 @@ -317,12 +315,12 @@
  24.100                  COVARIANT => (constraint :: cs, tye_idx)
  24.101                | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
  24.102                | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
  24.103 -                  handle NO_UNIFIER (msg, _) => 
  24.104 -                    err_list ctxt (gen_msg err 
  24.105 -                      "failed to unify invariant arguments w.r.t. to the known map function") 
  24.106 +                  handle NO_UNIFIER (msg, _) =>
  24.107 +                    err_list ctxt (gen_msg err
  24.108 +                      "failed to unify invariant arguments w.r.t. to the known map function")
  24.109                        (fst tye_idx) Ts)
  24.110                | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
  24.111 -                  handle NO_UNIFIER (msg, _) => 
  24.112 +                  handle NO_UNIFIER (msg, _) =>
  24.113                      error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
  24.114              val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
  24.115                (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
  24.116 @@ -359,7 +357,7 @@
  24.117              val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done;
  24.118              val todo' = ch @ todo;
  24.119            in
  24.120 -            if subsort (S', S) (*TODO check this*)
  24.121 +            if Sign.subsort thy (S', S) (*TODO check this*)
  24.122              then simplify done' todo' (tye', idx)
  24.123              else error (gen_msg err "sort mismatch")
  24.124            end
  24.125 @@ -394,11 +392,11 @@
  24.126      (* do simplification *)
  24.127  
  24.128      val (cs', tye_idx') = simplify_constraints cs tye_idx;
  24.129 -    
  24.130 -    fun find_error_pack lower T' = map_filter 
  24.131 +
  24.132 +    fun find_error_pack lower T' = map_filter
  24.133        (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
  24.134 -      
  24.135 -    fun find_cycle_packs nodes = 
  24.136 +
  24.137 +    fun find_cycle_packs nodes =
  24.138        let
  24.139          val (but_last, last) = split_last nodes
  24.140          val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
  24.141 @@ -431,7 +429,7 @@
  24.142          fun adjust T U = if super then (T, U) else (U, T);
  24.143          fun styp_test U Ts = forall
  24.144            (fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts;
  24.145 -        fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts
  24.146 +        fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts
  24.147        in
  24.148          forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts
  24.149        end;
  24.150 @@ -448,7 +446,7 @@
  24.151      *)
  24.152      fun tightest sup S styps_and_sorts (T :: Ts) =
  24.153        let
  24.154 -        fun restriction T = Type.of_sort tsig (t_of T, S)
  24.155 +        fun restriction T = Sign.of_sort thy (t_of T, S)
  24.156            andalso ex_styp_of_sort (not sup) T styps_and_sorts;
  24.157          fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
  24.158        in
  24.159 @@ -467,11 +465,11 @@
  24.160              val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
  24.161                handle Typ_Graph.CYCLES cycles =>
  24.162                  let
  24.163 -                  val (tye, idx) = 
  24.164 -                    fold 
  24.165 +                  val (tye, idx) =
  24.166 +                    fold
  24.167                        (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
  24.168 -                        handle NO_UNIFIER (msg, _) => 
  24.169 -                          err_bound ctxt 
  24.170 +                        handle NO_UNIFIER (msg, _) =>
  24.171 +                          err_bound ctxt
  24.172                              (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
  24.173                              (find_cycle_packs cycle)))
  24.174                        cycles tye_idx
  24.175 @@ -495,13 +493,13 @@
  24.176            in
  24.177              if not (is_typeT T) orelse not (is_typeT U) orelse T = U
  24.178              then if super then (hd nodes, T') else (T', hd nodes)
  24.179 -            else 
  24.180 -              if super andalso 
  24.181 +            else
  24.182 +              if super andalso
  24.183                  Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
  24.184 -              else if not super andalso 
  24.185 +              else if not super andalso
  24.186                  Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
  24.187                else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
  24.188 -                    (fst tye_idx) 
  24.189 +                    (fst tye_idx)
  24.190                      (maps find_cycle_packs cycles @ find_error_pack super T')
  24.191            end;
  24.192        in
  24.193 @@ -528,7 +526,7 @@
  24.194            val assignment =
  24.195              if null bound orelse null not_params then NONE
  24.196              else SOME (tightest lower S styps_and_sorts (map nameT not_params)
  24.197 -                handle BOUND_ERROR msg => 
  24.198 +                handle BOUND_ERROR msg =>
  24.199                    err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
  24.200          in
  24.201            (case assignment of
  24.202 @@ -560,7 +558,7 @@
  24.203            val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
  24.204              |> fold (assign_ub G) ts;
  24.205          in
  24.206 -          assign_alternating ts 
  24.207 +          assign_alternating ts
  24.208              (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
  24.209          end;
  24.210  
  24.211 @@ -573,7 +571,7 @@
  24.212            filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
  24.213          val to_unify = map (fn T => T :: get_preds G T) max_params;
  24.214        in
  24.215 -        fold 
  24.216 +        fold
  24.217            (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
  24.218              handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
  24.219            to_unify tye_idx
  24.220 @@ -686,24 +684,24 @@
  24.221              val (u', U, (tye, idx)) = inf bs u tye_idx';
  24.222              val V = Type_Infer.mk_param idx [];
  24.223              val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
  24.224 -              handle NO_UNIFIER (msg, tye') => 
  24.225 +              handle NO_UNIFIER (msg, tye') =>
  24.226                  raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
  24.227            in (tu, V, tye_idx'') end;
  24.228  
  24.229 -    fun infer_single t tye_idx = 
  24.230 +    fun infer_single t tye_idx =
  24.231        let val (t, _, tye_idx') = inf [] t tye_idx;
  24.232        in (t, tye_idx') end;
  24.233 -      
  24.234 +
  24.235      val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
  24.236 -      handle TYPE_INFERENCE_ERROR err =>     
  24.237 +      handle TYPE_INFERENCE_ERROR err =>
  24.238          let
  24.239            fun gen_single t (tye_idx, constraints) =
  24.240              let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
  24.241              in (tye_idx', constraints' @ constraints) end;
  24.242 -      
  24.243 +
  24.244            val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
  24.245            val (tye, idx) = process_constraints ctxt err constraints tye_idx;
  24.246 -        in 
  24.247 +        in
  24.248            (insert_coercions ctxt tye ts, (tye, idx))
  24.249          end);
  24.250  
  24.251 @@ -739,15 +737,15 @@
  24.252      val ctxt = Context.proof_of context;
  24.253      val t = singleton (Variable.polymorphic ctxt) raw_t;
  24.254  
  24.255 -    fun err_str t = "\n\nThe provided function has the type\n" ^ 
  24.256 -      Syntax.string_of_typ ctxt (fastype_of t) ^ 
  24.257 +    fun err_str t = "\n\nThe provided function has the type\n" ^
  24.258 +      Syntax.string_of_typ ctxt (fastype_of t) ^
  24.259        "\n\nThe general type signature of a map function is" ^
  24.260        "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
  24.261        "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
  24.262 -      
  24.263 +
  24.264      val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
  24.265        handle Empty => error ("Not a proper map function:" ^ err_str t);
  24.266 -    
  24.267 +
  24.268      fun gen_arg_var ([], []) = []
  24.269        | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
  24.270            if U = U' then
  24.271 @@ -756,8 +754,8 @@
  24.272            else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
  24.273            else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
  24.274            else error ("Functions do not apply to arguments correctly:" ^ err_str t)
  24.275 -      | gen_arg_var (_, Ts) = 
  24.276 -          if forall (op = andf is_stypeT o fst) Ts 
  24.277 +      | gen_arg_var (_, Ts) =
  24.278 +          if forall (op = andf is_stypeT o fst) Ts
  24.279            then map (INVARIANT_TO o fst) Ts
  24.280            else error ("Different numbers of functions and variant arguments\n" ^ err_str t);
  24.281