1.1 --- a/src/Pure/General/pretty.ML	Sun Apr 17 23:47:05 2011 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Mon Apr 18 11:13:29 2011 +0200
     1.3 @@ -64,18 +64,6 @@
     1.4    val writeln: T -> unit
     1.5    val to_ML: T -> ML_Pretty.pretty
     1.6    val from_ML: ML_Pretty.pretty -> T
     1.7 -  type pp
     1.8 -  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
     1.9 -  val term: pp -> term -> T
    1.10 -  val typ: pp -> typ -> T
    1.11 -  val sort: pp -> sort -> T
    1.12 -  val classrel: pp -> class list -> T
    1.13 -  val arity: pp -> arity -> T
    1.14 -  val string_of_term: pp -> term -> string
    1.15 -  val string_of_typ: pp -> typ -> string
    1.16 -  val string_of_sort: pp -> sort -> string
    1.17 -  val string_of_classrel: pp -> class list -> string
    1.18 -  val string_of_arity: pp -> arity -> string
    1.19  end;
    1.20  
    1.21  structure Pretty: PRETTY =
    1.22 @@ -332,27 +320,4 @@
    1.23  
    1.24  end;
    1.25  
    1.26 -
    1.27 -
    1.28 -(** abstract pretty printing context **)
    1.29 -
    1.30 -datatype pp =
    1.31 -  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
    1.32 -
    1.33 -val pp = PP;
    1.34 -
    1.35 -fun pp_fun f (PP x) = f x;
    1.36 -
    1.37 -val term     = pp_fun #1;
    1.38 -val typ      = pp_fun #2;
    1.39 -val sort     = pp_fun #3;
    1.40 -val classrel = pp_fun #4;
    1.41 -val arity    = pp_fun #5;
    1.42 -
    1.43 -val string_of_term     = string_of oo term;
    1.44 -val string_of_typ      = string_of oo typ;
    1.45 -val string_of_sort     = string_of oo sort;
    1.46 -val string_of_classrel = string_of oo classrel;
    1.47 -val string_of_arity    = string_of oo arity;
    1.48 -
    1.49  end;

     2.1 --- a/src/Pure/Isar/class.ML	Sun Apr 17 23:47:05 2011 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Mon Apr 18 11:13:29 2011 +0200
     2.3 @@ -529,14 +529,15 @@
     2.4      val primary_constraints = map (apsnd
     2.5        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     2.6      val algebra = Sign.classes_of thy
     2.7 -      |> fold (fn tyco => Sorts.add_arities (Syntax.pp_global thy)
     2.8 +      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
     2.9              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    2.10      val consts = Sign.consts_of thy;
    2.11      val improve_constraints = AList.lookup (op =)
    2.12        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
    2.13 -    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
    2.14 -     of NONE => NONE
    2.15 -      | SOME ts' => SOME (ts', ctxt);
    2.16 +    fun resort_check ts ctxt =
    2.17 +      (case resort_terms (Context.pretty ctxt) algebra consts improve_constraints ts of
    2.18 +        NONE => NONE
    2.19 +      | SOME ts' => SOME (ts', ctxt));
    2.20      val lookup_inst_param = AxClass.lookup_inst_param consts params;
    2.21      val typ_instance = Type.typ_instance (Sign.tsig_of thy);
    2.22      fun improve (c, ty) = case lookup_inst_param (c, ty)

     3.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 23:47:05 2011 +0200
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 11:13:29 2011 +0200
     3.3 @@ -302,7 +302,7 @@
     3.4    map_tsig (fn tsig as (local_tsig, global_tsig) =>
     3.5      let val thy_tsig = Sign.tsig_of thy in
     3.6        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
     3.7 -      else (Type.merge_tsig (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
     3.8 +      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
     3.9      end) |>
    3.10    map_consts (fn consts as (local_consts, global_consts) =>
    3.11      let val thy_consts = Sign.consts_of thy in
    3.12 @@ -376,7 +376,7 @@
    3.13  
    3.14  fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
    3.15    let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
    3.16 -  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
    3.17 +  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
    3.18  
    3.19  in
    3.20  
    3.21 @@ -546,7 +546,7 @@
    3.22  
    3.23  local
    3.24  
    3.25 -fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
    3.26 +fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
    3.27    (not (abbrev_mode ctxt)) (consts_of ctxt);
    3.28  
    3.29  fun expand_binds ctxt =
    3.30 @@ -666,9 +666,9 @@
    3.31  fun gen_cert prop ctxt t =
    3.32    t
    3.33    |> expand_abbrevs ctxt
    3.34 -  |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    3.35 -    handle TYPE (msg, _, _) => error msg
    3.36 -      | TERM (msg, _) => error msg);
    3.37 +  |> (fn t' =>
    3.38 +      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    3.39 +        handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
    3.40  
    3.41  in
    3.42  

     4.1 --- a/src/Pure/ROOT.ML	Sun Apr 17 23:47:05 2011 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Apr 18 11:13:29 2011 +0200
     4.3 @@ -53,6 +53,7 @@
     4.4  use "General/xml.ML";
     4.5  use "General/xml_data.ML";
     4.6  use "General/yxml.ML";
     4.7 +use "General/pretty.ML";
     4.8  
     4.9  use "General/sha1.ML";
    4.10  if String.isPrefix "polyml" ml_system
    4.11 @@ -103,7 +104,6 @@
    4.12  
    4.13  use "name.ML";
    4.14  use "term.ML";
    4.15 -use "General/pretty.ML";
    4.16  use "context.ML";
    4.17  use "config.ML";
    4.18  use "context_position.ML";

     5.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 23:47:05 2011 +0200
     5.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Apr 18 11:13:29 2011 +0200
     5.3 @@ -82,14 +82,13 @@
     5.4    val is_pretty_global: Proof.context -> bool
     5.5    val set_pretty_global: bool -> Proof.context -> Proof.context
     5.6    val init_pretty_global: theory -> Proof.context
     5.7 +  val init_pretty: Context.pretty -> Proof.context
     5.8    val pretty_term_global: theory -> term -> Pretty.T
     5.9    val pretty_typ_global: theory -> typ -> Pretty.T
    5.10    val pretty_sort_global: theory -> sort -> Pretty.T
    5.11    val string_of_term_global: theory -> term -> string
    5.12    val string_of_typ_global: theory -> typ -> string
    5.13    val string_of_sort_global: theory -> sort -> string
    5.14 -  val pp: Proof.context -> Pretty.pp
    5.15 -  val pp_global: theory -> Pretty.pp
    5.16    type syntax
    5.17    val eq_syntax: syntax * syntax -> bool
    5.18    val lookup_const: syntax -> string -> string option
    5.19 @@ -375,6 +374,7 @@
    5.20  fun is_pretty_global ctxt = Config.get ctxt pretty_global;
    5.21  val set_pretty_global = Config.put pretty_global;
    5.22  val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
    5.23 +val init_pretty = Context.pretty_context init_pretty_global;
    5.24  
    5.25  val pretty_term_global = pretty_term o init_pretty_global;
    5.26  val pretty_typ_global = pretty_typ o init_pretty_global;
    5.27 @@ -385,23 +385,6 @@
    5.28  val string_of_sort_global = string_of_sort o init_pretty_global;
    5.29  
    5.30  
    5.31 -(* pp operations -- deferred evaluation *)
    5.32 -
    5.33 -fun pp ctxt = Pretty.pp
    5.34 - (fn x => pretty_term ctxt x,
    5.35 -  fn x => pretty_typ ctxt x,
    5.36 -  fn x => pretty_sort ctxt x,
    5.37 -  fn x => pretty_classrel ctxt x,
    5.38 -  fn x => pretty_arity ctxt x);
    5.39 -
    5.40 -fun pp_global thy = Pretty.pp
    5.41 - (fn x => pretty_term_global thy x,
    5.42 -  fn x => pretty_typ_global thy x,
    5.43 -  fn x => pretty_sort_global thy x,
    5.44 -  fn x => pretty_classrel (init_pretty_global thy) x,
    5.45 -  fn x => pretty_arity (init_pretty_global thy) x);
    5.46 -
    5.47 -
    5.48  
    5.49  (** tables of translation functions **)
    5.50  

     6.1 --- a/src/Pure/axclass.ML	Sun Apr 17 23:47:05 2011 +0200
     6.2 +++ b/src/Pure/axclass.ML	Mon Apr 18 11:13:29 2011 +0200
     6.3 @@ -62,9 +62,12 @@
     6.4  fun add_param pp ((x, c): param) params =
     6.5    (case AList.lookup (op =) params x of
     6.6      NONE => (x, c) :: params
     6.7 -  | SOME c' => error ("Duplicate class parameter " ^ quote x ^
     6.8 -      " for " ^ Pretty.string_of_sort pp [c] ^
     6.9 -      (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
    6.10 +  | SOME c' =>
    6.11 +      let val ctxt = Syntax.init_pretty pp in
    6.12 +        error ("Duplicate class parameter " ^ quote x ^
    6.13 +          " for " ^ Syntax.string_of_sort ctxt [c] ^
    6.14 +          (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c']))
    6.15 +      end);
    6.16  
    6.17  
    6.18  (* setup data *)
    6.19 @@ -590,7 +593,7 @@
    6.20        |> #2
    6.21        |> Sign.restore_naming facts_thy
    6.22        |> map_axclasses (Symtab.update (class, axclass))
    6.23 -      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
    6.24 +      |> map_params (fold (fn (x, _) => add_param (Context.pretty ctxt) (x, class)) params);
    6.25  
    6.26    in (class, result_thy) end;
    6.27  

     7.1 --- a/src/Pure/consts.ML	Sun Apr 17 23:47:05 2011 +0200
     7.2 +++ b/src/Pure/consts.ML	Mon Apr 18 11:13:29 2011 +0200
     7.3 @@ -26,7 +26,7 @@
     7.4    val intern_syntax: T -> xstring -> string
     7.5    val extern_syntax: Proof.context -> T -> string -> xstring
     7.6    val read_const: T -> string -> term
     7.7 -  val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     7.8 +  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     7.9    val typargs: T -> string * typ -> typ list
    7.10    val instance: T -> string * typ list -> typ
    7.11    val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
    7.12 @@ -156,7 +156,8 @@
    7.13  fun certify pp tsig do_expand consts =
    7.14    let
    7.15      fun err msg (c, T) =
    7.16 -      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
    7.17 +      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
    7.18 +        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
    7.19      val certT = Type.cert_typ tsig;
    7.20      fun cert tm =
    7.21        let
    7.22 @@ -269,7 +270,7 @@
    7.23  
    7.24  fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
    7.25    let
    7.26 -    val pp = Syntax.pp ctxt;
    7.27 +    val pp = Context.pretty ctxt;
    7.28      val cert_term = certify pp tsig false consts;
    7.29      val expand_term = certify pp tsig true consts;
    7.30      val force_expand = mode = Print_Mode.internal;

     8.1 --- a/src/Pure/context.ML	Sun Apr 17 23:47:05 2011 +0200
     8.2 +++ b/src/Pure/context.ML	Mon Apr 18 11:13:29 2011 +0200
     8.3 @@ -28,6 +28,7 @@
     8.4  sig
     8.5    include BASIC_CONTEXT
     8.6    (*theory context*)
     8.7 +  type pretty
     8.8    val parents_of: theory -> theory list
     8.9    val ancestors_of: theory -> theory list
    8.10    val theory_name: theory -> string
    8.11 @@ -52,7 +53,7 @@
    8.12    val copy_thy: theory -> theory
    8.13    val checkpoint_thy: theory -> theory
    8.14    val finish_thy: theory -> theory
    8.15 -  val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    8.16 +  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    8.17    (*proof context*)
    8.18    val raw_transfer: theory -> Proof.context -> Proof.context
    8.19    (*generic context*)
    8.20 @@ -71,6 +72,10 @@
    8.21    val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    8.22    val theory_of: generic -> theory  (*total*)
    8.23    val proof_of: generic -> Proof.context  (*total*)
    8.24 +  (*pretty printing context*)
    8.25 +  val pretty: Proof.context -> pretty
    8.26 +  val pretty_global: theory -> pretty
    8.27 +  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    8.28    (*thread data*)
    8.29    val thread_data: unit -> generic option
    8.30    val the_thread_data: unit -> generic
    8.31 @@ -86,7 +91,7 @@
    8.32    structure Theory_Data:
    8.33    sig
    8.34      val declare: Object.T -> (Object.T -> Object.T) ->
    8.35 -      (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
    8.36 +      (pretty -> Object.T * Object.T -> Object.T) -> serial
    8.37      val get: serial -> (Object.T -> 'a) -> theory -> 'a
    8.38      val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
    8.39    end
    8.40 @@ -110,12 +115,14 @@
    8.41  (*private copy avoids potential conflict of table exceptions*)
    8.42  structure Datatab = Table(type key = int val ord = int_ord);
    8.43  
    8.44 +datatype pretty = Pretty of Object.T;
    8.45 +
    8.46  local
    8.47  
    8.48  type kind =
    8.49   {empty: Object.T,
    8.50    extend: Object.T -> Object.T,
    8.51 -  merge: Pretty.pp -> Object.T * Object.T -> Object.T};
    8.52 +  merge: pretty -> Object.T * Object.T -> Object.T};
    8.53  
    8.54  val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
    8.55  
    8.56 @@ -546,6 +553,16 @@
    8.57  val proof_of = cases Proof_Context.init_global I;
    8.58  
    8.59  
    8.60 +(* pretty printing context *)
    8.61 +
    8.62 +exception PRETTY of generic;
    8.63 +
    8.64 +val pretty = Pretty o PRETTY o Proof;
    8.65 +val pretty_global = Pretty o PRETTY o Theory;
    8.66 +
    8.67 +fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
    8.68 +
    8.69 +
    8.70  
    8.71  (** thread data **)
    8.72  
    8.73 @@ -593,7 +610,7 @@
    8.74    type T
    8.75    val empty: T
    8.76    val extend: T -> T
    8.77 -  val merge: Pretty.pp -> T * T -> T
    8.78 +  val merge: Context.pretty -> T * T -> T
    8.79  end;
    8.80  
    8.81  signature THEORY_DATA_ARGS =

     9.1 --- a/src/Pure/defs.ML	Sun Apr 17 23:47:05 2011 +0200
     9.2 +++ b/src/Pure/defs.ML	Mon Apr 18 11:13:29 2011 +0200
     9.3 @@ -7,7 +7,7 @@
     9.4  
     9.5  signature DEFS =
     9.6  sig
     9.7 -  val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
     9.8 +  val pretty_const: Context.pretty -> string * typ list -> Pretty.T
     9.9    val plain_args: typ list -> bool
    9.10    type T
    9.11    type spec =
    9.12 @@ -18,8 +18,8 @@
    9.13     {restricts: ((string * typ list) * string) list,
    9.14      reducts: ((string * typ list) * (string * typ list) list) list}
    9.15    val empty: T
    9.16 -  val merge: Pretty.pp -> T * T -> T
    9.17 -  val define: Pretty.pp -> bool -> string option -> string ->
    9.18 +  val merge: Context.pretty -> T * T -> T
    9.19 +  val define: Context.pretty -> bool -> string option -> string ->
    9.20      string * typ list -> (string * typ list) list -> T -> T
    9.21  end
    9.22  
    9.23 @@ -34,7 +34,9 @@
    9.24    let
    9.25      val prt_args =
    9.26        if null args then []
    9.27 -      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
    9.28 +      else
    9.29 +        [Pretty.list "(" ")"
    9.30 +          (map (Syntax.pretty_typ (Syntax.init_pretty pp) o Logic.unvarifyT_global) args)];
    9.31    in Pretty.block (Pretty.str c :: prt_args) end;
    9.32  
    9.33  fun plain_args args =

    10.1 --- a/src/Pure/display.ML	Sun Apr 17 23:47:05 2011 +0200
    10.2 +++ b/src/Pure/display.ML	Mon Apr 18 11:13:29 2011 +0200
    10.3 @@ -143,7 +143,7 @@
    10.4      fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
    10.5      val prt_term_no_vars = prt_term o Logic.unvarify_global;
    10.6      fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    10.7 -    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
    10.8 +    val prt_const' = Defs.pretty_const (Context.pretty ctxt);
    10.9  
   10.10      fun pretty_classrel (c, []) = prt_cls c
   10.11        | pretty_classrel (c, cs) = Pretty.block

    11.1 --- a/src/Pure/sign.ML	Sun Apr 17 23:47:05 2011 +0200
    11.2 +++ b/src/Pure/sign.ML	Mon Apr 18 11:13:29 2011 +0200
    11.3 @@ -61,7 +61,7 @@
    11.4    val certify_sort: theory -> sort -> sort
    11.5    val certify_typ: theory -> typ -> typ
    11.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
    11.7 -  val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
    11.8 +  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
    11.9    val certify_term: theory -> term -> term * typ * int
   11.10    val cert_term: theory -> term -> term
   11.11    val cert_prop: theory -> term -> term
   11.12 @@ -243,7 +243,7 @@
   11.13  (* certify wrt. type signature *)
   11.14  
   11.15  val arity_number = Type.arity_number o tsig_of;
   11.16 -fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
   11.17 +fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
   11.18  
   11.19  val certify_class         = Type.cert_class o tsig_of;
   11.20  val certify_sort          = Type.cert_sort o tsig_of;
   11.21 @@ -262,7 +262,7 @@
   11.22          val xs = map Free bs;           (*we do not rename here*)
   11.23          val t' = subst_bounds (xs, t);
   11.24          val u' = subst_bounds (xs, u);
   11.25 -        val msg = Type.appl_error pp t' T u' U;
   11.26 +        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
   11.27        in raise TYPE (msg, [T, U], [t', u']) end;
   11.28  
   11.29      fun typ_of (_, Const (_, T)) = T
   11.30 @@ -301,10 +301,11 @@
   11.31      val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   11.32    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   11.33  
   11.34 -fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
   11.35 -fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
   11.36 +fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
   11.37 +fun cert_term_abbrev thy =
   11.38 +  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
   11.39  val cert_term = #1 oo certify_term;
   11.40 -fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
   11.41 +fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
   11.42  
   11.43  end;
   11.44  
   11.45 @@ -457,12 +458,12 @@
   11.46    thy |> map_sign (fn (naming, syn, tsig, consts) =>
   11.47      let
   11.48        val ctxt = Syntax.init_pretty_global thy;
   11.49 -      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
   11.50 +      val tsig' = Type.add_class ctxt (Context.pretty ctxt) naming (bclass, classes) tsig;
   11.51      in (naming, syn, tsig', consts) end)
   11.52    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   11.53  
   11.54 -fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
   11.55 -fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
   11.56 +fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
   11.57 +fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
   11.58  
   11.59  
   11.60  (* add translation functions *)

    12.1 --- a/src/Pure/sorts.ML	Sun Apr 17 23:47:05 2011 +0200
    12.2 +++ b/src/Pure/sorts.ML	Mon Apr 18 11:13:29 2011 +0200
    12.3 @@ -40,15 +40,15 @@
    12.4    val minimal_sorts: algebra -> sort list -> sort Ord_List.T
    12.5    val certify_class: algebra -> class -> class    (*exception TYPE*)
    12.6    val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
    12.7 -  val add_class: Pretty.pp -> class * class list -> algebra -> algebra
    12.8 -  val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
    12.9 -  val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
   12.10 +  val add_class: Context.pretty -> class * class list -> algebra -> algebra
   12.11 +  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
   12.12 +  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
   12.13    val empty_algebra: algebra
   12.14 -  val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
   12.15 -  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
   12.16 +  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
   12.17 +  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
   12.18      -> algebra -> (sort -> sort) * algebra
   12.19    type class_error
   12.20 -  val class_error: Pretty.pp -> class_error -> string
   12.21 +  val class_error: Context.pretty -> class_error -> string
   12.22    exception CLASS_ERROR of class_error
   12.23    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   12.24    val meet_sort: algebra -> typ * sort
   12.25 @@ -200,7 +200,7 @@
   12.26  
   12.27  fun err_cyclic_classes pp css =
   12.28    error (cat_lines (map (fn cs =>
   12.29 -    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
   12.30 +    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
   12.31  
   12.32  fun add_class pp (c, cs) = map_classes (fn classes =>
   12.33    let
   12.34 @@ -217,12 +217,12 @@
   12.35  
   12.36  fun for_classes _ NONE = ""
   12.37    | for_classes pp (SOME (c1, c2)) =
   12.38 -      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
   12.39 +      " for classes " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2];
   12.40  
   12.41  fun err_conflict pp t cc (c, Ss) (c', Ss') =
   12.42    error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
   12.43 -    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
   12.44 -    Pretty.string_of_arity pp (t, Ss', [c']));
   12.45 +    Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss, [c]) ^ " and\n  " ^
   12.46 +    Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss', [c']));
   12.47  
   12.48  fun coregular pp algebra t (c, Ss) ars =
   12.49    let
   12.50 @@ -336,12 +336,13 @@
   12.51    No_Subsort of sort * sort;
   12.52  
   12.53  fun class_error pp (No_Classrel (c1, c2)) =
   12.54 -      "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
   12.55 +      "No class relation " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) [c1, c2]
   12.56    | class_error pp (No_Arity (a, c)) =
   12.57 -      "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
   12.58 +      "No type arity " ^ Syntax.string_of_arity (Syntax.init_pretty pp) (a, [], [c])
   12.59    | class_error pp (No_Subsort (S1, S2)) =
   12.60 -     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
   12.61 -       ^ " < " ^ Pretty.string_of_sort pp S2;
   12.62 +      "Cannot derive subsort relation " ^
   12.63 +      Syntax.string_of_sort (Syntax.init_pretty pp) S1 ^ " < " ^
   12.64 +      Syntax.string_of_sort (Syntax.init_pretty pp) S2;
   12.65  
   12.66  exception CLASS_ERROR of class_error;
   12.67  

    13.1 --- a/src/Pure/theory.ML	Sun Apr 17 23:47:05 2011 +0200
    13.2 +++ b/src/Pure/theory.ML	Mon Apr 18 11:13:29 2011 +0200
    13.3 @@ -137,7 +137,7 @@
    13.4  
    13.5  fun begin_theory name imports =
    13.6    let
    13.7 -    val thy = Context.begin_thy Syntax.pp_global name imports;
    13.8 +    val thy = Context.begin_thy Context.pretty_global name imports;
    13.9      val wrappers = begin_wrappers thy;
   13.10    in
   13.11      thy
   13.12 @@ -196,7 +196,7 @@
   13.13        else error ("Specification depends on extra type variables: " ^
   13.14          commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
   13.15          "\nThe error(s) above occurred in " ^ quote description);
   13.16 -  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
   13.17 +  in Defs.define (Context.pretty ctxt) unchecked def description (prep lhs) (map prep rhs) end;
   13.18  
   13.19  fun add_deps ctxt a raw_lhs raw_rhs thy =
   13.20    let

    14.1 --- a/src/Pure/type.ML	Sun Apr 17 23:47:05 2011 +0200
    14.2 +++ b/src/Pure/type.ML	Mon Apr 18 11:13:29 2011 +0200
    14.3 @@ -11,7 +11,7 @@
    14.4    val mark_polymorphic: typ -> typ
    14.5    val constraint: typ -> term -> term
    14.6    val strip_constraints: term -> term
    14.7 -  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
    14.8 +  val appl_error: Proof.context -> term -> typ -> term -> typ -> string
    14.9    (*type signatures and certified types*)
   14.10    datatype decl =
   14.11      LogicalType of int |
   14.12 @@ -55,7 +55,7 @@
   14.13    val cert_typ_mode: mode -> tsig -> typ -> typ
   14.14    val cert_typ: tsig -> typ -> typ
   14.15    val arity_number: tsig -> string -> int
   14.16 -  val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
   14.17 +  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
   14.18  
   14.19    (*special treatment of type vars*)
   14.20    val sort_of_atyp: typ -> sort
   14.21 @@ -86,7 +86,7 @@
   14.22    val eq_type: tyenv -> typ * typ -> bool
   14.23  
   14.24    (*extend and merge type signatures*)
   14.25 -  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
   14.26 +  val add_class: Proof.context -> Context.pretty -> Name_Space.naming ->
   14.27      binding * class list -> tsig -> tsig
   14.28    val hide_class: bool -> string -> tsig -> tsig
   14.29    val set_defsort: sort -> tsig -> tsig
   14.30 @@ -94,9 +94,9 @@
   14.31    val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   14.32    val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   14.33    val hide_type: bool -> string -> tsig -> tsig
   14.34 -  val add_arity: Pretty.pp -> arity -> tsig -> tsig
   14.35 -  val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   14.36 -  val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
   14.37 +  val add_arity: Context.pretty -> arity -> tsig -> tsig
   14.38 +  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
   14.39 +  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
   14.40  end;
   14.41  
   14.42  structure Type: TYPE =
   14.43 @@ -116,15 +116,15 @@
   14.44    | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
   14.45    | strip_constraints a = a;
   14.46  
   14.47 -fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
   14.48 +fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
   14.49        cat_lines
   14.50         ["Failed to meet type constraint:", "",
   14.51          Pretty.string_of (Pretty.block
   14.52 -         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
   14.53 -          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
   14.54 +         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u,
   14.55 +          Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]),
   14.56          Pretty.string_of (Pretty.block
   14.57 -         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
   14.58 -  | appl_error pp t T u U =
   14.59 +         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])]
   14.60 +  | appl_error ctxt t T u U =
   14.61        cat_lines
   14.62         ["Type error in application: " ^
   14.63            (case T of
   14.64 @@ -132,11 +132,11 @@
   14.65            | _ => "operator not of function type"),
   14.66          "",
   14.67          Pretty.string_of (Pretty.block
   14.68 -          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
   14.69 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
   14.70 +          [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t,
   14.71 +            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]),
   14.72          Pretty.string_of (Pretty.block
   14.73 -          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
   14.74 -            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
   14.75 +          [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u,
   14.76 +            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])];
   14.77  
   14.78  
   14.79  

    15.1 --- a/src/Pure/type_infer.ML	Sun Apr 17 23:47:05 2011 +0200
    15.2 +++ b/src/Pure/type_infer.ML	Mon Apr 18 11:13:29 2011 +0200
    15.3 @@ -289,7 +289,7 @@
    15.4  
    15.5  fun infer ctxt =
    15.6    let
    15.7 -    val pp = Syntax.pp ctxt;
    15.8 +    val pp = Context.pretty ctxt;
    15.9  
   15.10  
   15.11      (* errors *)
   15.12 @@ -310,7 +310,7 @@
   15.13  
   15.14      fun err_appl msg tye bs t T u U =
   15.15        let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
   15.16 -      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
   15.17 +      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
   15.18  
   15.19  
   15.20      (* main *)

    16.1 --- a/src/Tools/Code/code_preproc.ML	Sun Apr 17 23:47:05 2011 +0200
    16.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 11:13:29 2011 +0200
    16.3 @@ -431,7 +431,7 @@
    16.4        |> fold (ensure_fun thy arities eqngr) cs
    16.5        |> fold (ensure_rhs thy arities eqngr) cs_rhss;
    16.6      val arities' = fold (add_arity thy vardeps) insts arities;
    16.7 -    val pp = Syntax.pp_global thy;
    16.8 +    val pp = Context.pretty_global thy;
    16.9      val algebra = Sorts.subalgebra pp (is_proper_class thy)
   16.10        (AList.lookup (op =) arities') (Sign.classes_of thy);
   16.11      val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);

    17.1 --- a/src/Tools/Code/code_thingol.ML	Sun Apr 17 23:47:05 2011 +0200
    17.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 11:13:29 2011 +0200
    17.3 @@ -582,7 +582,7 @@
    17.4  
    17.5  fun not_wellsorted thy permissive some_thm ty sort e =
    17.6    let
    17.7 -    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
    17.8 +    val err_class = Sorts.class_error (Context.pretty_global thy) e;
    17.9      val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
   17.10        ^ Syntax.string_of_sort_global thy sort;
   17.11    in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;

    18.1 --- a/src/Tools/subtyping.ML	Sun Apr 17 23:47:05 2011 +0200
    18.2 +++ b/src/Tools/subtyping.ML	Mon Apr 18 11:13:29 2011 +0200
    18.3 @@ -98,7 +98,7 @@
    18.4  fun unify weak ctxt =
    18.5    let
    18.6      val thy = Proof_Context.theory_of ctxt;
    18.7 -    val pp = Syntax.pp ctxt;
    18.8 +    val pp = Context.pretty ctxt;
    18.9      val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
   18.10  
   18.11  
   18.12 @@ -190,8 +190,8 @@
   18.13  
   18.14  (** error messages **)
   18.15  
   18.16 -fun gen_msg err msg = 
   18.17 -  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
   18.18 +fun gen_msg err msg =
   18.19 +  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
   18.20    (if msg = "" then "" else ": " ^ msg) ^ "\n";
   18.21  
   18.22  fun prep_output ctxt tye bs ts Ts =
   18.23 @@ -204,27 +204,26 @@
   18.24    in (map prep ts', Ts') end;
   18.25  
   18.26  fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
   18.27 -  
   18.28 +
   18.29  fun unif_failed msg =
   18.30    "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
   18.31 -  
   18.32 +
   18.33  fun err_appl_msg ctxt msg tye bs t T u U () =
   18.34    let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
   18.35 -  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
   18.36 +  in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end;
   18.37  
   18.38  fun err_list ctxt msg tye Ts =
   18.39    let
   18.40      val (_, Ts') = prep_output ctxt tye [] [] Ts;
   18.41 -    val text = cat_lines ([msg,
   18.42 -      "Cannot unify a list of types that should be the same:",
   18.43 -      (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
   18.44 +    val text =
   18.45 +      msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^
   18.46 +        Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts'));
   18.47    in
   18.48      error text
   18.49    end;
   18.50  
   18.51  fun err_bound ctxt msg tye packs =
   18.52    let
   18.53 -    val pp = Syntax.pp ctxt;
   18.54      val (ts, Ts) = fold
   18.55        (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
   18.56          let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
   18.57 @@ -233,9 +232,10 @@
   18.58      val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
   18.59          (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
   18.60            Pretty.block [
   18.61 -            Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
   18.62 -            Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
   18.63 -            Pretty.block [Pretty.term pp (t $ u)]]))
   18.64 +            Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2,
   18.65 +            Syntax.pretty_typ ctxt U, Pretty.brk 3,
   18.66 +            Pretty.str "from function application", Pretty.brk 2,
   18.67 +            Pretty.block [Syntax.pretty_term ctxt (t $ u)]]))
   18.68          ts Ts))
   18.69    in
   18.70      error text
   18.71 @@ -280,7 +280,7 @@
   18.72      val coes_graph = coes_graph_of ctxt;
   18.73      val tmaps = tmaps_of ctxt;
   18.74      val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
   18.75 -    val pp = Syntax.pp ctxt;
   18.76 +    val pp = Context.pretty ctxt;
   18.77      val arity_sorts = Type.arity_sorts pp tsig;
   18.78      val subsort = Type.subsort tsig;
   18.79  
   18.80 @@ -289,9 +289,9 @@
   18.81            (case pairself f (fst c) of
   18.82              (false, false) => apsnd (cons c) (split_cs f cs)
   18.83            | _ => apfst (cons c) (split_cs f cs));
   18.84 -          
   18.85 +
   18.86      fun unify_list (T :: Ts) tye_idx =
   18.87 -      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;      
   18.88 +      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
   18.89  
   18.90  
   18.91      (* check whether constraint simplification will terminate using weak unification *)
   18.92 @@ -317,12 +317,12 @@
   18.93                  COVARIANT => (constraint :: cs, tye_idx)
   18.94                | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
   18.95                | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
   18.96 -                  handle NO_UNIFIER (msg, _) => 
   18.97 -                    err_list ctxt (gen_msg err 
   18.98 -                      "failed to unify invariant arguments w.r.t. to the known map function") 
   18.99 +                  handle NO_UNIFIER (msg, _) =>
  18.100 +                    err_list ctxt (gen_msg err
  18.101 +                      "failed to unify invariant arguments w.r.t. to the known map function")
  18.102                        (fst tye_idx) Ts)
  18.103                | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
  18.104 -                  handle NO_UNIFIER (msg, _) => 
  18.105 +                  handle NO_UNIFIER (msg, _) =>
  18.106                      error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
  18.107              val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
  18.108                (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
  18.109 @@ -394,11 +394,11 @@
  18.110      (* do simplification *)
  18.111  
  18.112      val (cs', tye_idx') = simplify_constraints cs tye_idx;
  18.113 -    
  18.114 -    fun find_error_pack lower T' = map_filter 
  18.115 +
  18.116 +    fun find_error_pack lower T' = map_filter
  18.117        (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
  18.118 -      
  18.119 -    fun find_cycle_packs nodes = 
  18.120 +
  18.121 +    fun find_cycle_packs nodes =
  18.122        let
  18.123          val (but_last, last) = split_last nodes
  18.124          val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
  18.125 @@ -467,11 +467,11 @@
  18.126              val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
  18.127                handle Typ_Graph.CYCLES cycles =>
  18.128                  let
  18.129 -                  val (tye, idx) = 
  18.130 -                    fold 
  18.131 +                  val (tye, idx) =
  18.132 +                    fold
  18.133                        (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
  18.134 -                        handle NO_UNIFIER (msg, _) => 
  18.135 -                          err_bound ctxt 
  18.136 +                        handle NO_UNIFIER (msg, _) =>
  18.137 +                          err_bound ctxt
  18.138                              (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
  18.139                              (find_cycle_packs cycle)))
  18.140                        cycles tye_idx
  18.141 @@ -495,13 +495,13 @@
  18.142            in
  18.143              if not (is_typeT T) orelse not (is_typeT U) orelse T = U
  18.144              then if super then (hd nodes, T') else (T', hd nodes)
  18.145 -            else 
  18.146 -              if super andalso 
  18.147 +            else
  18.148 +              if super andalso
  18.149                  Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
  18.150 -              else if not super andalso 
  18.151 +              else if not super andalso
  18.152                  Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
  18.153                else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
  18.154 -                    (fst tye_idx) 
  18.155 +                    (fst tye_idx)
  18.156                      (maps find_cycle_packs cycles @ find_error_pack super T')
  18.157            end;
  18.158        in
  18.159 @@ -528,7 +528,7 @@
  18.160            val assignment =
  18.161              if null bound orelse null not_params then NONE
  18.162              else SOME (tightest lower S styps_and_sorts (map nameT not_params)
  18.163 -                handle BOUND_ERROR msg => 
  18.164 +                handle BOUND_ERROR msg =>
  18.165                    err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
  18.166          in
  18.167            (case assignment of
  18.168 @@ -560,7 +560,7 @@
  18.169            val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
  18.170              |> fold (assign_ub G) ts;
  18.171          in
  18.172 -          assign_alternating ts 
  18.173 +          assign_alternating ts
  18.174              (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
  18.175          end;
  18.176  
  18.177 @@ -573,7 +573,7 @@
  18.178            filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
  18.179          val to_unify = map (fn T => T :: get_preds G T) max_params;
  18.180        in
  18.181 -        fold 
  18.182 +        fold
  18.183            (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
  18.184              handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
  18.185            to_unify tye_idx
  18.186 @@ -686,24 +686,24 @@
  18.187              val (u', U, (tye, idx)) = inf bs u tye_idx';
  18.188              val V = Type_Infer.mk_param idx [];
  18.189              val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
  18.190 -              handle NO_UNIFIER (msg, tye') => 
  18.191 +              handle NO_UNIFIER (msg, tye') =>
  18.192                  raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
  18.193            in (tu, V, tye_idx'') end;
  18.194  
  18.195 -    fun infer_single t tye_idx = 
  18.196 +    fun infer_single t tye_idx =
  18.197        let val (t, _, tye_idx') = inf [] t tye_idx;
  18.198        in (t, tye_idx') end;
  18.199 -      
  18.200 +
  18.201      val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
  18.202 -      handle TYPE_INFERENCE_ERROR err =>     
  18.203 +      handle TYPE_INFERENCE_ERROR err =>
  18.204          let
  18.205            fun gen_single t (tye_idx, constraints) =
  18.206              let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
  18.207              in (tye_idx', constraints' @ constraints) end;
  18.208 -      
  18.209 +
  18.210            val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
  18.211            val (tye, idx) = process_constraints ctxt err constraints tye_idx;
  18.212 -        in 
  18.213 +        in
  18.214            (insert_coercions ctxt tye ts, (tye, idx))
  18.215          end);
  18.216  
  18.217 @@ -739,15 +739,15 @@
  18.218      val ctxt = Context.proof_of context;
  18.219      val t = singleton (Variable.polymorphic ctxt) raw_t;
  18.220  
  18.221 -    fun err_str t = "\n\nThe provided function has the type\n" ^ 
  18.222 -      Syntax.string_of_typ ctxt (fastype_of t) ^ 
  18.223 +    fun err_str t = "\n\nThe provided function has the type\n" ^
  18.224 +      Syntax.string_of_typ ctxt (fastype_of t) ^
  18.225        "\n\nThe general type signature of a map function is" ^
  18.226        "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
  18.227        "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
  18.228 -      
  18.229 +
  18.230      val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
  18.231        handle Empty => error ("Not a proper map function:" ^ err_str t);
  18.232 -    
  18.233 +
  18.234      fun gen_arg_var ([], []) = []
  18.235        | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
  18.236            if U = U' then
  18.237 @@ -756,8 +756,8 @@
  18.238            else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
  18.239            else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
  18.240            else error ("Functions do not apply to arguments correctly:" ^ err_str t)
  18.241 -      | gen_arg_var (_, Ts) = 
  18.242 -          if forall (op = andf is_stypeT o fst) Ts 
  18.243 +      | gen_arg_var (_, Ts) =
  18.244 +          if forall (op = andf is_stypeT o fst) Ts
  18.245            then map (INVARIANT_TO o fst) Ts
  18.246            else error ("Different numbers of functions and variant arguments\n" ^ err_str t);
  18.247