improved output; refer to Pretty.pp;
authorwenzelm
Sat May 29 15:03:59 2004 +0200 (2004-05-29)
changeset 1482815d12761ba54
parent 14827 d973e7f820cb
child 14829 cfa5fe01a7b7
improved output; refer to Pretty.pp;
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat May 29 15:02:35 2004 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat May 29 15:03:59 2004 +0200
     1.3 @@ -15,13 +15,20 @@
     1.4    exception CONTEXT of string * context
     1.5    val theory_of: context -> theory
     1.6    val sign_of: context -> Sign.sg
     1.7 -  val syntax_of: context -> Syntax.syntax * string list * string list
     1.8 +  val is_fixed: context -> string -> bool
     1.9    val fixed_names_of: context -> string list
    1.10    val assumptions_of: context -> (cterm list * exporter) list
    1.11    val prems_of: context -> thm list
    1.12    val print_proof_data: theory -> unit
    1.13    val init: theory -> context
    1.14 -  val is_fixed: context -> string -> bool
    1.15 +  val pretty_term: context -> term -> Pretty.T
    1.16 +  val pretty_typ: context -> typ -> Pretty.T
    1.17 +  val pretty_sort: context -> sort -> Pretty.T
    1.18 +  val pp: context -> Pretty.pp
    1.19 +  val pretty_thm: context -> thm -> Pretty.T
    1.20 +  val pretty_thms: context -> thm list -> Pretty.T
    1.21 +  val pretty_fact: context -> string * thm list -> Pretty.T
    1.22 +  val string_of_term: context -> term -> string
    1.23    val default_type: context -> string -> typ option
    1.24    val used_types: context -> string list
    1.25    val read_typ: context -> string -> typ
    1.26 @@ -123,13 +130,6 @@
    1.27    val add_cases: (string * RuleCases.T) list -> context -> context
    1.28    val apply_case: RuleCases.T -> context
    1.29      -> context * ((indexname * term option) list * (string * term list) list)
    1.30 -  val pretty_term: context -> term -> Pretty.T
    1.31 -  val pretty_typ: context -> typ -> Pretty.T
    1.32 -  val pretty_sort: context -> sort -> Pretty.T
    1.33 -  val pretty_thm: context -> thm -> Pretty.T
    1.34 -  val pretty_thms: context -> thm list -> Pretty.T
    1.35 -  val pretty_fact: context -> string * thm list -> Pretty.T
    1.36 -  val string_of_term: context -> term -> string
    1.37    val verbose: bool ref
    1.38    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.39    val print_syntax: context -> unit
    1.40 @@ -379,6 +379,33 @@
    1.41  
    1.42  
    1.43  
    1.44 +(** pretty printing **)
    1.45 +
    1.46 +fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt;
    1.47 +val pretty_typ = Sign.pretty_typ o sign_of;
    1.48 +val pretty_sort = Sign.pretty_sort o sign_of;
    1.49 +
    1.50 +fun pp ctxt = Pretty.pp (pretty_term ctxt) (pretty_typ ctxt) (pretty_sort ctxt)
    1.51 +  (Sign.pretty_classrel (sign_of ctxt)) (Sign.pretty_arity (sign_of ctxt));
    1.52 +
    1.53 +val string_of_term = Pretty.string_of oo pretty_term;
    1.54 +
    1.55 +fun pretty_thm ctxt thm =
    1.56 +  if ! Display.show_hyps then
    1.57 +    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
    1.58 +  else pretty_term ctxt (Thm.prop_of thm);
    1.59 +
    1.60 +fun pretty_thms ctxt [th] = pretty_thm ctxt th
    1.61 +  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
    1.62 +
    1.63 +fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
    1.64 +  | pretty_fact ctxt (a, [th]) =
    1.65 +      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
    1.66 +  | pretty_fact ctxt (a, ths) =
    1.67 +      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
    1.68 +
    1.69 +
    1.70 +
    1.71  (** default sorts and types **)
    1.72  
    1.73  fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi);
    1.74 @@ -474,28 +501,29 @@
    1.75  
    1.76  (* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
    1.77  
    1.78 -fun read_def_termTs freeze syn sg (types, sorts, used) sTs =
    1.79 -  Sign.read_def_terms' syn (sg, types, sorts) used freeze sTs;
    1.80 +fun read_def_termTs freeze pp syn sg (types, sorts, used) sTs =
    1.81 +  Sign.read_def_terms' pp syn (sg, types, sorts) used freeze sTs;
    1.82  
    1.83 -fun read_def_termT freeze syn sg defs sT = apfst hd (read_def_termTs freeze syn sg defs [sT]);
    1.84 +fun read_def_termT freeze pp syn sg defs sT =
    1.85 +  apfst hd (read_def_termTs freeze pp syn sg defs [sT]);
    1.86 +
    1.87 +fun read_term_sg freeze pp syn sg defs s =
    1.88 +  #1 (read_def_termT freeze pp syn sg defs (s, TypeInfer.logicT));
    1.89  
    1.90 -fun read_term_sg freeze syn sg defs s =
    1.91 -  #1 (read_def_termT freeze syn sg defs (s, TypeInfer.logicT));
    1.92 -
    1.93 -fun read_prop_sg freeze syn sg defs s = #1 (read_def_termT freeze syn sg defs (s, propT));
    1.94 +fun read_prop_sg freeze pp syn sg defs s =
    1.95 +  #1 (read_def_termT freeze pp syn sg defs (s, propT));
    1.96  
    1.97 -fun read_terms_sg freeze syn sg defs =
    1.98 -  #1 o read_def_termTs freeze syn sg defs o map (rpair TypeInfer.logicT);
    1.99 +fun read_terms_sg freeze pp syn sg defs =
   1.100 +  #1 o read_def_termTs freeze pp syn sg defs o map (rpair TypeInfer.logicT);
   1.101  
   1.102 -fun read_props_sg freeze syn sg defs = #1 o read_def_termTs freeze syn sg defs o map (rpair propT);
   1.103 +fun read_props_sg freeze pp syn sg defs =
   1.104 +  #1 o read_def_termTs freeze pp syn sg defs o map (rpair propT);
   1.105  
   1.106  
   1.107 -fun cert_term_sg sg t = Thm.term_of (Thm.cterm_of sg t);
   1.108 +fun cert_term_sg pp sg t = #1 (Sign.certify_term pp sg t);
   1.109  
   1.110 -fun cert_prop_sg sg tm =
   1.111 -  let
   1.112 -    val ctm = Thm.cterm_of sg tm;
   1.113 -    val {t, T, ...} = Thm.rep_cterm ctm;
   1.114 +fun cert_prop_sg pp sg tm =
   1.115 +  let val (t, T, _) = Sign.certify_term pp sg tm
   1.116    in if T = propT then t else raise TERM ("Term not of type prop", [t]) end;
   1.117  
   1.118  
   1.119 @@ -556,7 +584,7 @@
   1.120      val sorts = append_env (def_sort ctxt) more_sorts;
   1.121      val used = used_types ctxt @ more_used;
   1.122    in
   1.123 -    (transform_error (read (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s
   1.124 +    (transform_error (read (pp ctxt) (syn_of ctxt) (sign_of ctxt) (types, sorts, used)) s
   1.125        handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
   1.126          | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
   1.127      |> app (intern_skolem ctxt internal)
   1.128 @@ -595,7 +623,8 @@
   1.129  
   1.130  fun gen_cert cert pattern schematic ctxt t = t
   1.131    |> (if pattern then I else norm_term ctxt schematic)
   1.132 -  |> (fn t' => cert (sign_of ctxt) t' handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
   1.133 +  |> (fn t' => cert (pp ctxt) (sign_of ctxt) t'
   1.134 +    handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
   1.135  
   1.136  in
   1.137  
   1.138 @@ -661,30 +690,6 @@
   1.139  
   1.140  
   1.141  
   1.142 -(** pretty printing **)
   1.143 -
   1.144 -fun pretty_term ctxt = Sign.pretty_term' (syn_of ctxt) (sign_of ctxt) o context_tr' ctxt;
   1.145 -val pretty_typ = Sign.pretty_typ o sign_of;
   1.146 -val pretty_sort = Sign.pretty_sort o sign_of;
   1.147 -
   1.148 -val string_of_term = Pretty.string_of oo pretty_term;
   1.149 -
   1.150 -fun pretty_thm ctxt thm =
   1.151 -  if ! Display.show_hyps then
   1.152 -    Display.pretty_thm_aux (pretty_sort ctxt, pretty_term ctxt) false thm
   1.153 -  else pretty_term ctxt (Thm.prop_of thm);
   1.154 -
   1.155 -fun pretty_thms ctxt [th] = pretty_thm ctxt th
   1.156 -  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
   1.157 -
   1.158 -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
   1.159 -  | pretty_fact ctxt (a, [th]) =
   1.160 -      Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, pretty_thm ctxt th]
   1.161 -  | pretty_fact ctxt (a, ths) =
   1.162 -      Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths));
   1.163 -
   1.164 -
   1.165 -
   1.166  (** Hindley-Milner polymorphism **)
   1.167  
   1.168  (* warn_extra_tfrees *)
     2.1 --- a/src/Pure/sign.ML	Sat May 29 15:02:35 2004 +0200
     2.2 +++ b/src/Pure/sign.ML	Sat May 29 15:03:59 2004 +0200
     2.3 @@ -78,36 +78,38 @@
     2.4    val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
     2.5    val pretty_typ: sg -> typ -> Pretty.T
     2.6    val pretty_sort: sg -> sort -> Pretty.T
     2.7 -  val pretty_classrel: sg -> class * class -> Pretty.T
     2.8 -  val pretty_arity: sg -> string * sort list * sort -> Pretty.T
     2.9 +  val pretty_classrel: sg -> class list -> Pretty.T
    2.10 +  val pretty_arity: sg -> arity -> Pretty.T
    2.11    val string_of_term: sg -> term -> string
    2.12    val string_of_typ: sg -> typ -> string
    2.13    val string_of_sort: sg -> sort -> string
    2.14 -  val str_of_sort: sg -> sort -> string
    2.15 -  val str_of_classrel: sg -> class * class -> string
    2.16 -  val str_of_arity: sg -> string * sort list * sort -> string
    2.17 +  val string_of_classrel: sg -> class list -> string
    2.18 +  val string_of_arity: sg -> arity -> string
    2.19    val pprint_term: sg -> term -> pprint_args -> unit
    2.20    val pprint_typ: sg -> typ -> pprint_args -> unit
    2.21 +  val pp: sg -> Pretty.pp
    2.22    val certify_class: sg -> class -> class
    2.23    val certify_sort: sg -> sort -> sort
    2.24    val certify_typ: sg -> typ -> typ
    2.25    val certify_typ_raw: sg -> typ -> typ
    2.26    val certify_tyname: sg -> string -> string
    2.27    val certify_const: sg -> string -> string
    2.28 -  val certify_term: sg -> term -> term * typ * int
    2.29 +  val certify_term: Pretty.pp -> sg -> term -> term * typ * int
    2.30    val read_sort: sg -> string -> sort
    2.31    val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
    2.32    val read_typ: sg * (indexname -> sort option) -> string -> typ
    2.33    val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    2.34    val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    2.35 -  val infer_types: sg -> (indexname -> typ option) ->
    2.36 +  val inst_typ_tvars: sg -> (indexname * typ) list -> typ -> typ
    2.37 +  val inst_term_tvars: sg -> (indexname * typ) list -> term -> term
    2.38 +  val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
    2.39      (indexname -> sort option) -> string list -> bool
    2.40      -> xterm list * typ -> term * (indexname * typ) list
    2.41 -  val infer_types_simult: sg -> (indexname -> typ option) ->
    2.42 +  val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
    2.43      (indexname -> sort option) -> string list -> bool
    2.44      -> (xterm list * typ) list -> term list * (indexname * typ) list
    2.45 -  val read_def_terms':
    2.46 -    Syntax.syntax -> sg * (indexname -> typ option) * (indexname -> sort option) ->
    2.47 +  val read_def_terms': Pretty.pp -> Syntax.syntax ->
    2.48 +    sg * (indexname -> typ option) * (indexname -> sort option) ->
    2.49      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
    2.50    val read_def_terms:
    2.51      sg * (indexname -> typ option) * (indexname -> sort option) ->
    2.52 @@ -337,6 +339,7 @@
    2.53  val typ_instance = Type.typ_instance o tsig_of;
    2.54  
    2.55  
    2.56 +
    2.57  (** signature data **)
    2.58  
    2.59  (* errors *)
    2.60 @@ -603,8 +606,8 @@
    2.61    Syntax.pretty_sort (syn_of sg)
    2.62      (if ! NameSpace.long_names then S else extrn_sort spaces S);
    2.63  
    2.64 -fun pretty_classrel sg (c1, c2) = Pretty.block
    2.65 -  [pretty_sort sg [c1], Pretty.str " <", Pretty.brk 1, pretty_sort sg [c2]];
    2.66 +fun pretty_classrel sg cs = Pretty.block (flat
    2.67 +  (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs)));
    2.68  
    2.69  fun pretty_arity sg (t, Ss, S) =
    2.70    let
    2.71 @@ -617,17 +620,18 @@
    2.72        ([Pretty.str (t' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
    2.73    end;
    2.74  
    2.75 -fun string_of_term sg t = Pretty.string_of (pretty_term sg t);
    2.76 -fun string_of_typ sg T = Pretty.string_of (pretty_typ sg T);
    2.77 -fun string_of_sort sg S = Pretty.string_of (pretty_sort sg S);
    2.78 -
    2.79 -fun str_of_sort sg S = Pretty.str_of (pretty_sort sg S);
    2.80 -fun str_of_classrel sg c1_c2 = Pretty.str_of (pretty_classrel sg c1_c2);
    2.81 -fun str_of_arity sg ar = Pretty.str_of (pretty_arity sg ar);
    2.82 +val string_of_term = Pretty.string_of oo pretty_term;
    2.83 +val string_of_typ = Pretty.string_of oo pretty_typ;
    2.84 +val string_of_sort = Pretty.string_of oo pretty_sort;
    2.85 +val string_of_classrel = Pretty.string_of oo pretty_classrel;
    2.86 +val string_of_arity = Pretty.string_of oo pretty_arity;
    2.87  
    2.88  fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
    2.89  fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
    2.90  
    2.91 +fun pp sg = Pretty.pp (pretty_term sg) (pretty_typ sg) (pretty_sort sg)
    2.92 +  (pretty_classrel sg) (pretty_arity sg);
    2.93 +
    2.94  
    2.95  
    2.96  (** read sorts **)  (*exception ERROR*)
    2.97 @@ -741,17 +745,15 @@
    2.98    in nodups (([], []), ([], [])) tm; tm end;
    2.99  
   2.100  (*compute and check type of the term*)
   2.101 -fun type_check sg tm =
   2.102 +fun type_check pp sg tm =
   2.103    let
   2.104 -    val prt = setmp Syntax.show_brackets true (pretty_term sg);
   2.105 -    val prT = pretty_typ sg;
   2.106 -
   2.107      fun err_appl why bs t T u U =
   2.108        let
   2.109          val xs = map Free bs;           (*we do not rename here*)
   2.110          val t' = subst_bounds (xs, t);
   2.111          val u' = subst_bounds (xs, u);
   2.112 -        val text = cat_lines (TypeInfer.appl_error prt prT why t' T u' U);
   2.113 +        val text = cat_lines
   2.114 +          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
   2.115        in raise TYPE (text, [T, U], [t', u']) end;
   2.116  
   2.117      fun typ_of (_, Const (_, T)) = T
   2.118 @@ -764,13 +766,13 @@
   2.119            let val T = typ_of (bs, t) and U = typ_of (bs, u) in
   2.120              (case T of
   2.121                Type ("fun", [T1, T2]) =>
   2.122 -                if T1 = U then T2 else err_appl "Incompatible operand type." bs t T u U
   2.123 -            | _ => err_appl "Operator not of function type." bs t T u U)
   2.124 +                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
   2.125 +            | _ => err_appl "Operator not of function type" bs t T u U)
   2.126            end;
   2.127  
   2.128    in typ_of ([], tm) end;
   2.129  
   2.130 -fun certify_term sg tm =
   2.131 +fun certify_term pp sg tm =
   2.132    let
   2.133      val _ = check_stale sg;
   2.134  
   2.135 @@ -779,7 +781,7 @@
   2.136  
   2.137      fun err msg = raise TYPE (msg, [], [tm']);
   2.138  
   2.139 -    fun show_const a T = quote a ^ " :: " ^ quote (string_of_typ sg T);
   2.140 +    fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T;
   2.141  
   2.142      fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
   2.143        | check_atoms (Abs (_, _, t)) = check_atoms t
   2.144 @@ -795,11 +797,18 @@
   2.145    in
   2.146      check_atoms tm';
   2.147      nodup_vars tm';
   2.148 -    (tm', type_check sg tm', maxidx_of_term tm')
   2.149 +    (tm', type_check pp sg tm', maxidx_of_term tm')
   2.150    end;
   2.151  
   2.152  
   2.153  
   2.154 +(** instantiation **)
   2.155 +
   2.156 +fun inst_typ_tvars sg = Type.inst_typ_tvars (pp sg) (tsig_of sg);
   2.157 +fun inst_term_tvars sg = Type.inst_term_tvars (pp sg) (tsig_of sg);
   2.158 +
   2.159 +
   2.160 +
   2.161  (** infer_types **)         (*exception ERROR*)
   2.162  
   2.163  (*
   2.164 @@ -812,19 +821,17 @@
   2.165    typs: expected types
   2.166  *)
   2.167  
   2.168 -fun infer_types_simult sg def_type def_sort used freeze args =
   2.169 +fun infer_types_simult pp sg def_type def_sort used freeze args =
   2.170    let
   2.171      val tsig = tsig_of sg;
   2.172 -    val prt = setmp Syntax.show_brackets true (pretty_term sg);
   2.173 -    val prT = pretty_typ sg;
   2.174  
   2.175      val termss = foldr multiply (map fst args, [[]]);
   2.176      val typs =
   2.177        map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   2.178  
   2.179 -    fun infer ts = OK
   2.180 -      (TypeInfer.infer_types prt prT tsig (const_type sg) def_type def_sort
   2.181 -        (intern_const sg) (intern_tycons sg) (intern_sort sg) used freeze typs ts)
   2.182 +    fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig
   2.183 +        (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg)
   2.184 +        (intern_sort sg) used freeze typs ts)
   2.185        handle TYPE (msg, _, _) => Error msg;
   2.186  
   2.187      val err_results = map infer termss;
   2.188 @@ -847,27 +854,27 @@
   2.189            \You may still want to disambiguate your grammar or your input."
   2.190        else (); hd results)
   2.191      else (ambig_msg (); error ("More than one term is type correct:\n" ^
   2.192 -      (cat_lines (map (Pretty.string_of o prt) (flat (map fst results))))))
   2.193 +      cat_lines (map (Pretty.string_of_term pp) (flat (map fst results)))))
   2.194    end;
   2.195  
   2.196  
   2.197 -fun infer_types sg def_type def_sort used freeze tsT =
   2.198 -  apfst hd (infer_types_simult sg def_type def_sort used freeze [tsT]);
   2.199 +fun infer_types pp sg def_type def_sort used freeze tsT =
   2.200 +  apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]);
   2.201  
   2.202  
   2.203  (** read_def_terms **)
   2.204  
   2.205  (*read terms, infer types*)
   2.206 -fun read_def_terms' syn (sign, types, sorts) used freeze sTs =
   2.207 +fun read_def_terms' pp syn (sign, types, sorts) used freeze sTs =
   2.208    let
   2.209      fun read (s, T) =
   2.210        let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
   2.211        in (Syntax.read syn T' s, T') end;
   2.212      val tsTs = map read sTs;
   2.213 -  in infer_types_simult sign types sorts used freeze tsTs end;
   2.214 +  in infer_types_simult pp sign types sorts used freeze tsTs end;
   2.215  
   2.216  fun read_def_terms (sign, types, sorts) =
   2.217 -  read_def_terms' (syn_of sign) (sign, types, sorts);
   2.218 +  read_def_terms' (pp sign) (syn_of sign) (sign, types, sorts);
   2.219  
   2.220  fun simple_read_term sign T s =
   2.221    (read_def_terms (sign, K None, K None) [] true [(s, T)]
   2.222 @@ -946,7 +953,7 @@
   2.223      val prepS = prep_sort sg syn tsig spaces;
   2.224      fun prep_arity (c, Ss, S) =
   2.225        (if int then intrn spaces typeK c else c, map prepS Ss, prepS S);
   2.226 -    val tsig' = Type.add_arities (map prep_arity arities) tsig;
   2.227 +    val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
   2.228      val log_types = Type.logical_types tsig';
   2.229    in
   2.230      (map_syntax (Syntax.extend_log_types log_types) syn,
   2.231 @@ -1027,16 +1034,16 @@
   2.232    in
   2.233      ext_consts_i sg
   2.234        (map_syntax (Syntax.extend_consts names) syn,
   2.235 -        Type.add_classes classes' tsig, ctab, (path, spaces'), data)
   2.236 +        Type.add_classes (pp sg) classes' tsig, ctab, (path, spaces'), data)
   2.237      consts
   2.238    end;
   2.239  
   2.240  
   2.241  (* add to classrel *)
   2.242  
   2.243 -fun ext_classrel int _ (syn, tsig, ctab, (path, spaces), data) pairs =
   2.244 +fun ext_classrel int sg (syn, tsig, ctab, (path, spaces), data) pairs =
   2.245    let val intrn = if int then map (pairself (intrn_class spaces)) else I in
   2.246 -    (syn, Type.add_classrel (intrn pairs) tsig, ctab, (path, spaces), data)
   2.247 +    (syn, Type.add_classrel (pp sg) (intrn pairs) tsig, ctab, (path, spaces), data)
   2.248    end;
   2.249  
   2.250  
   2.251 @@ -1213,7 +1220,7 @@
   2.252        val stamps = merge_stamps stamps1 stamps2;
   2.253        val syntax = Syntax.merge_syntaxes syntax1 syntax2;
   2.254        val trfuns = merge_trfuns trfuns1 trfuns2;
   2.255 -      val tsig = Type.merge_tsigs (tsig1, tsig2);
   2.256 +      val tsig = Type.merge_tsigs (pp sg1) (tsig1, tsig2);   (* FIXME improve pp *)
   2.257        val consts = Symtab.merge eq_snd (consts1, consts2)
   2.258          handle Symtab.DUPS cs => err_dup_consts cs;
   2.259  
     3.1 --- a/src/Pure/sorts.ML	Sat May 29 15:02:35 2004 +0200
     3.2 +++ b/src/Pure/sorts.ML	Sat May 29 15:03:59 2004 +0200
     3.3 @@ -7,8 +7,6 @@
     3.4  
     3.5  signature SORTS =
     3.6  sig
     3.7 -  val str_of_sort: sort -> string
     3.8 -  val str_of_arity: string * sort list * sort -> string
     3.9    val eq_sort: sort * sort -> bool
    3.10    val mem_sort: sort * sort list -> bool
    3.11    val subset_sort: sort list * sort list -> bool
    3.12 @@ -31,8 +29,8 @@
    3.13    val of_sort: classes * arities -> typ * sort -> bool
    3.14    exception DOMAIN of string * class
    3.15    val mg_domain: classes * arities -> string -> sort -> sort list  (*exception DOMAIN*)
    3.16 -  val witness_sorts: classes * arities -> string list
    3.17 -    -> sort list -> sort list -> (typ * sort) list
    3.18 +  val witness_sorts: classes * arities -> string list ->
    3.19 +    sort list -> sort list -> (typ * sort) list
    3.20  end;
    3.21  
    3.22  structure Sorts: SORTS =
    3.23 @@ -53,16 +51,6 @@
    3.24  *)
    3.25  
    3.26  
    3.27 -(* simple printing -- lacks pretty printing, translations etc. *)
    3.28 -
    3.29 -fun str_of_sort [c] = c
    3.30 -  | str_of_sort cs = Library.enclose "{" "}" (Library.commas cs);
    3.31 -
    3.32 -fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S
    3.33 -  | str_of_arity (t, Ss, S) = t ^ " :: " ^
    3.34 -      Library.enclose "(" ")" (Library.commas (map str_of_sort Ss)) ^ " " ^ str_of_sort S;
    3.35 -
    3.36 -
    3.37  (* equality, membership and insertion of sorts *)
    3.38  
    3.39  fun eq_sort ([]: sort, []) = true
    3.40 @@ -190,7 +178,9 @@
    3.41  
    3.42  (** witness_sorts **)
    3.43  
    3.44 -fun witness_sorts_aux (classes, arities) log_types hyps sorts =
    3.45 +local
    3.46 +
    3.47 +fun witness_aux (classes, arities) log_types hyps sorts =
    3.48    let
    3.49      val top_witn = (propT, []);
    3.50      fun le S1 S2 = sort_le classes (S1, S2);
    3.51 @@ -229,6 +219,10 @@
    3.52  
    3.53    in witn_sorts [] (([], []), sorts) end;
    3.54  
    3.55 +fun str_of_sort [c] = c
    3.56 +  | str_of_sort cs = enclose "{" "}" (commas cs);
    3.57 +
    3.58 +in
    3.59  
    3.60  fun witness_sorts (classes, arities) log_types hyps sorts =
    3.61    let
    3.62 @@ -237,7 +231,8 @@
    3.63        | check_result (Some (T, S)) =
    3.64            if of_sort (classes, arities) (T, S) then Some (T, S)
    3.65            else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S);
    3.66 -  in mapfilter check_result (#2 (witness_sorts_aux (classes, arities) log_types hyps sorts)) end;
    3.67 -
    3.68 +  in mapfilter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end;
    3.69  
    3.70  end;
    3.71 +
    3.72 +end;
     4.1 --- a/src/Pure/theory.ML	Sat May 29 15:02:35 2004 +0200
     4.2 +++ b/src/Pure/theory.ML	Sat May 29 15:03:59 2004 +0200
     4.3 @@ -260,7 +260,7 @@
     4.4  
     4.5  fun cert_axm sg (name, raw_tm) =
     4.6    let
     4.7 -    val (t, T, _) = Sign.certify_term sg raw_tm
     4.8 +    val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
     4.9        handle TYPE (msg, _, _) => error msg
    4.10             | TERM (msg, _) => error msg;
    4.11    in
    4.12 @@ -273,15 +273,15 @@
    4.13  fun read_def_axm (sg, types, sorts) used (name, str) =
    4.14    let
    4.15      val ts = Syntax.read (Sign.syn_of sg) propT str;
    4.16 -    val (t, _) = Sign.infer_types sg types sorts used true (ts, propT);
    4.17 +    val (t, _) = Sign.infer_types (Sign.pp sg) sg types sorts used true (ts, propT);
    4.18    in cert_axm sg (name, t) end
    4.19    handle ERROR => err_in_axm name;
    4.20  
    4.21  fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str;
    4.22  
    4.23  fun inferT_axm sg (name, pre_tm) =
    4.24 -  let
    4.25 -    val (t, _) = Sign.infer_types sg (K None) (K None) [] true ([pre_tm], propT);
    4.26 +  let val (t, _) = Sign.infer_types (Sign.pp sg) sg
    4.27 +    (K None) (K None) [] true ([pre_tm], propT);
    4.28    in (name, no_vars sg t) end
    4.29    handle ERROR => err_in_axm name;
    4.30  
    4.31 @@ -510,7 +510,7 @@
    4.32  
    4.33  local
    4.34    fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
    4.35 -  val cert_term = #1 oo Sign.certify_term;
    4.36 +  fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
    4.37  in
    4.38  val add_finals = ext_finals read_term;
    4.39  val add_finals_i = ext_finals cert_term;
     5.1 --- a/src/Pure/thm.ML	Sat May 29 15:02:35 2004 +0200
     5.2 +++ b/src/Pure/thm.ML	Sat May 29 15:03:59 2004 +0200
     5.3 @@ -176,7 +176,7 @@
     5.4  
     5.5  (*create a cterm by checking a "raw" term with respect to a signature*)
     5.6  fun cterm_of sign tm =
     5.7 -  let val (t, T, maxidx) = Sign.certify_term sign tm
     5.8 +  let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm
     5.9    in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
    5.10    end;
    5.11  
    5.12 @@ -972,8 +972,8 @@
    5.13    | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
    5.14    let val (newsign_ref,tpairs) = foldr add_ctpair (ctpairs, (sign_ref,[]));
    5.15        val (newsign_ref,vTs) = foldr add_ctyp (vcTs, (newsign_ref,[]));
    5.16 -      val tsig = Sign.tsig_of (Sign.deref newsign_ref);
    5.17 -      fun subst t = subst_atomic tpairs (Type.inst_term_tvars tsig vTs t);
    5.18 +      fun subst t =
    5.19 +        subst_atomic tpairs (Sign.inst_term_tvars (Sign.deref newsign_ref) vTs t);
    5.20        val newprop = subst prop;
    5.21        val newdpairs = map (pairself subst) dpairs;
    5.22        val newth =
    5.23 @@ -1460,7 +1460,8 @@
    5.24        let
    5.25          val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
    5.26          val sign' = Sign.deref sign_ref';
    5.27 -        val (prop, T, maxidx) = Sign.certify_term sign' (oracle (sign', exn));
    5.28 +        val (prop, T, maxidx) =
    5.29 +          Sign.certify_term (Sign.pp sign') sign' (oracle (sign', exn));
    5.30        in
    5.31          if T <> propT then
    5.32            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
     6.1 --- a/src/Pure/type_infer.ML	Sat May 29 15:02:35 2004 +0200
     6.2 +++ b/src/Pure/type_infer.ML	Sat May 29 15:03:59 2004 +0200
     6.3 @@ -10,14 +10,13 @@
     6.4    val anyT: sort -> typ
     6.5    val logicT: typ
     6.6    val polymorphicT: typ -> typ
     6.7 -  val appl_error: (term -> Pretty.T) -> (typ -> Pretty.T)
     6.8 -    -> string -> term -> typ -> term -> typ -> string list
     6.9 +  val appl_error: Pretty.pp -> string -> term -> typ -> term -> typ -> string list
    6.10    val constrain: term -> typ -> term
    6.11    val param: int -> string * sort -> typ
    6.12    val paramify_dummies: int * typ -> int * typ
    6.13    val get_sort: Type.tsig -> (indexname -> sort option) -> (sort -> sort)
    6.14      -> (indexname * sort) list -> indexname -> sort
    6.15 -  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
    6.16 +  val infer_types: Pretty.pp
    6.17      -> Type.tsig -> (string -> typ option) -> (indexname -> typ option)
    6.18      -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
    6.19      -> (sort -> sort) -> string list -> bool -> typ list -> term list
    6.20 @@ -253,16 +252,16 @@
    6.21  exception NO_UNIFIER of string;
    6.22  
    6.23  
    6.24 -fun unify classes arities =
    6.25 +fun unify pp classes arities =
    6.26    let
    6.27  
    6.28      (* adjust sorts of parameters *)
    6.29  
    6.30      fun not_in_sort x S' S =
    6.31 -      "Variable " ^ x ^ "::" ^ Sorts.str_of_sort S' ^ " not of sort " ^
    6.32 -        Sorts.str_of_sort S ^ ".";
    6.33 +      "Variable " ^ x ^ "::" ^ Pretty.string_of_sort pp S' ^ " not of sort " ^
    6.34 +        Pretty.string_of_sort pp S;
    6.35  
    6.36 -    fun no_domain (a, c) = "No way to get " ^ a ^ "::" ^ c ^ ".";
    6.37 +    fun no_domain (a, c) = "No way to get " ^ Pretty.string_of_arity pp (a, [], [c]);
    6.38  
    6.39      fun meet (_, []) = ()
    6.40        | meet (Link (r as (ref (Param S'))), S) =
    6.41 @@ -304,7 +303,7 @@
    6.42        | unif (T, Link (ref U)) = unif (T, U)
    6.43        | unif (PType (a, Ts), PType (b, Us)) =
    6.44            if a <> b then
    6.45 -            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b ^ ".")
    6.46 +            raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b)
    6.47            else seq2 unif (Ts, Us)
    6.48        | unif (T, U) = if T = U then () else raise NO_UNIFIER "";
    6.49  
    6.50 @@ -314,24 +313,26 @@
    6.51  
    6.52  (** type inference **)
    6.53  
    6.54 -fun appl_error prt prT why t T u U =
    6.55 +fun appl_error pp why t T u U =
    6.56   ["Type error in application: " ^ why,
    6.57    "",
    6.58    Pretty.string_of (Pretty.block
    6.59 -    [Pretty.str "Operator:", Pretty.brk 2, prt t, Pretty.str " ::", Pretty.brk 1, prT T]),
    6.60 +    [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
    6.61 +      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
    6.62    Pretty.string_of (Pretty.block
    6.63 -    [Pretty.str "Operand:", Pretty.brk 3, prt u, Pretty.str " ::", Pretty.brk 1, prT U]),
    6.64 +    [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
    6.65 +      Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
    6.66    ""];
    6.67  
    6.68  
    6.69  (* infer *)                                     (*DESTRUCTIVE*)
    6.70  
    6.71 -fun infer prt prT classes arities =
    6.72 +fun infer pp classes arities =
    6.73    let
    6.74      (* errors *)
    6.75  
    6.76      fun unif_failed msg =
    6.77 -      "Type unification failed" ^ (if msg = "" then "." else ": " ^ msg) ^ "\n";
    6.78 +      "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n";
    6.79  
    6.80      fun prep_output bs ts Ts =
    6.81        let
    6.82 @@ -349,10 +350,9 @@
    6.83          val ([t', u'], [T', U']) = prep_output bs [t, u] [T, U];
    6.84          val why =
    6.85            (case T' of
    6.86 -            Type ("fun", _) => "Incompatible operand type."
    6.87 -          | _ => "Operator not of function type.");
    6.88 -        val text = unif_failed msg ^
    6.89 -                   cat_lines (appl_error prt prT why t' T' u' U');
    6.90 +            Type ("fun", _) => "Incompatible operand type"
    6.91 +          | _ => "Operator not of function type");
    6.92 +        val text = unif_failed msg ^ cat_lines (appl_error pp why t' T' u' U');
    6.93        in raise TYPE (text, [T', U'], [t', u']) end;
    6.94  
    6.95      fun err_constraint msg bs t T U =
    6.96 @@ -361,17 +361,17 @@
    6.97          val text = cat_lines
    6.98           [unif_failed msg,
    6.99            "Cannot meet type constraint:", "",
   6.100 -          Pretty.string_of
   6.101 -           (Pretty.block [Pretty.str "Term:", Pretty.brk 2, prt t',
   6.102 -                          Pretty.str " ::", Pretty.brk 1, prT T']),
   6.103 -          Pretty.string_of
   6.104 -           (Pretty.block [Pretty.str "Type:", Pretty.brk 2, prT U']), ""];
   6.105 +          Pretty.string_of (Pretty.block
   6.106 +           [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp t',
   6.107 +            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T']),
   6.108 +          Pretty.string_of (Pretty.block
   6.109 +           [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp U']), ""];
   6.110        in raise TYPE (text, [T', U'], [t']) end;
   6.111  
   6.112  
   6.113      (* main *)
   6.114  
   6.115 -    val unif = unify classes arities;
   6.116 +    val unif = unify pp classes arities;
   6.117  
   6.118      fun inf _ (PConst (_, T)) = T
   6.119        | inf _ (PFree (_, T)) = T
   6.120 @@ -397,7 +397,7 @@
   6.121  
   6.122  (* basic_infer_types *)
   6.123  
   6.124 -fun basic_infer_types prt prT const_type classes arities used freeze is_param ts Ts =
   6.125 +fun basic_infer_types pp const_type classes arities used freeze is_param ts Ts =
   6.126    let
   6.127      (*convert to preterms/typs*)
   6.128      val (Tps, Ts') = pretyps_of (K true) ([], Ts);
   6.129 @@ -405,7 +405,7 @@
   6.130  
   6.131      (*run type inference*)
   6.132      val tTs' = ListPair.map Constraint (ts', Ts');
   6.133 -    val _ = seq (fn t => (infer prt prT classes arities t; ())) tTs';
   6.134 +    val _ = seq (fn t => (infer pp classes arities t; ())) tTs';
   6.135  
   6.136      (*collect result unifier*)
   6.137      fun ch_var (xi, Link (r as ref (Param S))) = (r := PTVar (xi, S); None)
   6.138 @@ -452,11 +452,9 @@
   6.139        xi = xi' andalso Type.eq_sort tsig (S, S');
   6.140  
   6.141      val env = gen_distinct eq (map (apsnd map_sort) raw_env);
   6.142 -    val _ =
   6.143 -      (case gen_duplicates eq_fst env of
   6.144 -        [] => ()
   6.145 -      | dups => error ("Inconsistent sort constraints for type variable(s) " ^
   6.146 -          commas (map (quote o Syntax.string_of_vname' o fst) dups)));
   6.147 +    val _ = (case gen_duplicates eq_fst env of [] => ()
   6.148 +      | dups => error ("Inconsistent sort constraints for type variable(s) "
   6.149 +          ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
   6.150  
   6.151      fun get xi =
   6.152        (case (assoc (env, xi), def_sort xi) of
   6.153 @@ -516,7 +514,7 @@
   6.154    used: list of already used type variables
   6.155    freeze: if true then generated parameters are turned into TFrees, else TVars*)
   6.156  
   6.157 -fun infer_types prt prT tsig const_type def_type def_sort
   6.158 +fun infer_types pp tsig const_type def_type def_sort
   6.159      map_const map_type map_sort used freeze pat_Ts raw_ts =
   6.160    let
   6.161      val {classes, arities, ...} = Type.rep_tsig tsig;
   6.162 @@ -524,7 +522,7 @@
   6.163      val is_const = is_some o const_type;
   6.164      val raw_ts' =
   6.165        map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
   6.166 -    val (ts, Ts, unifier) = basic_infer_types prt prT const_type
   6.167 +    val (ts, Ts, unifier) = basic_infer_types pp const_type
   6.168        classes arities used freeze is_param raw_ts' pat_Ts';
   6.169    in (ts, unifier) end;
   6.170