--- a/src/Pure/General/name_space.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/General/name_space.ML Tue Oct 04 19:01:37 2005 +0200
@@ -50,7 +50,7 @@
val custom_accesses: (string list -> string list list) -> naming -> naming
val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
naming -> naming
- type 'a table = T * 'a Symtab.table
+ type 'a table (*= T * 'a Symtab.table*)
val empty_table: 'a table
val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
--- a/src/Pure/General/pretty.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/General/pretty.ML Tue Oct 04 19:01:37 2005 +0200
@@ -78,7 +78,7 @@
datatype T =
Block of T list * int * int | (*body, indentation, length*)
String of string * int | (*text, length*)
- Break of bool * int; (*mandatory flag, width if not taken*);
+ Break of bool * int; (*mandatory flag, width if not taken*)
@@ -88,19 +88,21 @@
val add_indent = Buffer.add o output_spaces;
fun set_indent wd = Buffer.empty |> add_indent wd;
-val empty =
+type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
+
+val empty: text =
{tx = Buffer.empty,
ind = Buffer.empty,
pos = 0,
nl = 0};
-fun newline {tx, ind, pos, nl} =
+fun newline {tx, ind, pos, nl} : text =
{tx = Buffer.add (Output.output "\n") tx,
ind = Buffer.empty,
pos = 0,
nl = nl + 1};
-fun string (s, len) {tx, ind, pos: int, nl} =
+fun string (s, len) {tx, ind, pos: int, nl} : text =
{tx = Buffer.add s tx,
ind = Buffer.add s ind,
pos = pos + len,
@@ -108,7 +110,7 @@
fun blanks wd = string (output_spaces wd, wd);
-fun indentation (buf, len) {tx, ind, pos, nl} =
+fun indentation (buf, len) {tx, ind, pos, nl} : text =
let val s = Buffer.content buf in
{tx = Buffer.add (Output.indent (s, len)) tx,
ind = Buffer.add s ind,
@@ -160,7 +162,7 @@
val block' =
if pos' < emergencypos then (ind |> add_indent indent, pos')
else (set_indent pos'', pos'');
- val btext = format (bes, block', breakdist (es, after)) text;
+ val btext: text = format (bes, block', breakdist (es, after)) text;
(*if this block was broken then force the next break*)
val es2 = if nl < #nl btext then forcenext es else es;
in format (es2, block, after) btext end
--- a/src/Pure/General/stack.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/General/stack.ML Tue Oct 04 19:01:37 2005 +0200
@@ -7,7 +7,7 @@
signature STACK =
sig
- type 'a T = 'a * 'a list
+ type 'a T (*= 'a * 'a list*)
val level: 'a T -> int
val init: 'a -> 'a T
val top: 'a T -> 'a
--- a/src/Pure/General/symbol.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/General/symbol.ML Tue Oct 04 19:01:37 2005 +0200
@@ -132,7 +132,7 @@
| is_ascii_quasi _ = false;
val is_ascii_blank =
- fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true
+ fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
| _ => false;
@@ -389,8 +389,8 @@
local
val scan_encoded_newline =
- $$ "\r" -- $$ "\n" >> K "\n" ||
- $$ "\r" >> K "\n" ||
+ $$ "\^M" -- $$ "\n" >> K "\n" ||
+ $$ "\^M" >> K "\n" ||
$$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
val scan_raw =
@@ -422,7 +422,7 @@
fun no_explode [] = true
| no_explode ("\\" :: "<" :: _) = false
- | no_explode ("\r" :: _) = false
+ | no_explode ("\^M" :: _) = false
| no_explode (_ :: cs) = no_explode cs;
fun sym_explode str =
--- a/src/Pure/General/xml.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/General/xml.ML Tue Oct 04 19:01:37 2005 +0200
@@ -47,11 +47,11 @@
| encode "\"" = """
| encode c = c;
-fun encode_charref c = "&#"^Int.toString (Char.ord c)^ ";"
+fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
val text = Library.translate_string encode
-val text_charref = implode o (map encode_charref) o String.explode
+val text_charref = translate_string encode_charref;
val cdata = enclose "<![CDATA[" "]]>\n"
--- a/src/Pure/Isar/attrib.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Oct 04 19:01:37 2005 +0200
@@ -282,7 +282,7 @@
val ctxt = init context;
val thy = ProofContext.theory_of ctxt;
- val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
+ val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
val internal_insts = term_insts |> List.mapPartial
(fn (xi, Args.Term t) => SOME (xi, t)
| (_, Args.Name _) => NONE
--- a/src/Pure/Isar/find_theorems.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML Tue Oct 04 19:01:37 2005 +0200
@@ -218,7 +218,7 @@
fun opt_not x = if isSome x then NONE else SOME (0, 0);
-fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y)
+fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
| opt_add _ _ = NONE;
in
--- a/src/Pure/Isar/isar_output.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Tue Oct 04 19:01:37 2005 +0200
@@ -206,22 +206,21 @@
(* command spans *)
type command = string * Position.T * string list; (*name, position, tags*)
-type tok = token * string * int; (*token, markup flag, meta-comment depth*)
-type source = tok list;
+type source = (token * (string * int)) list; (*token, markup flag, meta-comment depth*)
datatype span = Span of command * (source * source * source * source) * bool;
fun make_span cmd src =
let
- fun take_newline ((tok: tok) :: toks) =
- if newline_token (#1 tok) then ([tok], toks, true)
+ fun take_newline (tok :: toks) =
+ if newline_token (fst tok) then ([tok], toks, true)
else ([], tok :: toks, false)
| take_newline [] = ([], [], false);
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
src
- |> take_prefix (improper_token o #1)
- ||>> take_suffix (improper_token o #1)
- ||>> take_prefix (comment_token o #1)
+ |> take_prefix (improper_token o fst)
+ ||>> take_suffix (improper_token o fst)
+ ||>> take_prefix (comment_token o fst)
||> take_newline;
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
@@ -246,7 +245,7 @@
fun present_span lex default_tags span state state'
(tag_stack, active_tag, newline, buffer, present_cont) =
let
- val present = fold (fn (tok, flag, 0) =>
+ val present = fold (fn (tok, (flag, 0)) =>
Buffer.add (output_token lex state' tok)
#> Buffer.add flag
| _ => I);
@@ -332,7 +331,7 @@
(* tokens *)
val ignored = Scan.state --| ignore
- >> (fn d => (NONE, (NoToken, "", d)));
+ >> (fn d => (NONE, (NoToken, ("", d))));
fun markup mark mk flag = Scan.peek (fn d =>
improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
@@ -340,21 +339,21 @@
P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
>> (fn (((tok, pos), tags), txt) =>
let val name = T.val_of tok
- in (SOME (name, pos, tags), (mk (name, txt), flag, d)) end));
+ in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
val command = Scan.peek (fn d =>
P.position (Scan.one (T.is_kind T.Command)) --
Scan.repeat tag
>> (fn ((tok, pos), tags) =>
let val name = T.val_of tok
- in (SOME (name, pos, tags), (BasicToken tok, Latex.markup_false, d)) end));
+ in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
val cmt = Scan.peek (fn d =>
P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
- >> (fn txt => (NONE, (MarkupToken ("cmt", txt), "", d))));
+ >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
val other = Scan.peek (fn d =>
- Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, "", d))));
+ Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
val token =
ignored ||
@@ -367,15 +366,15 @@
(* spans *)
val stopper =
- ((NONE, (BasicToken (#1 T.stopper), "", 0)),
- fn (_, (BasicToken x, _, _)) => #2 T.stopper x | _ => false);
+ ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
+ fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
- val cmd = Scan.one (is_some o #1);
- val non_cmd = Scan.one (is_none o #1 andf not o #2 stopper) >> #2;
+ val cmd = Scan.one (is_some o fst);
+ val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
- val comments = Scan.any (comment_token o #1 o #2);
- val blank = Scan.one (blank_token o #1 o #2);
- val newline = Scan.one (newline_token o #1 o #2);
+ val comments = Scan.any (comment_token o fst o snd);
+ val blank = Scan.one (blank_token o fst o snd);
+ val newline = Scan.one (newline_token o fst o snd);
val before_cmd =
Scan.option (newline -- comments) --
Scan.option (newline -- comments) --
@@ -384,9 +383,9 @@
val span =
Scan.repeat non_cmd -- cmd --
Scan.repeat (Scan.unless before_cmd non_cmd) --
- Scan.option (newline >> (single o #2))
+ Scan.option (newline >> (single o snd))
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
- make_span (the cmd) (toks1 @ tok2 :: toks3 @ the_default [] tok4));
+ make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
val spans =
src
--- a/src/Pure/Isar/locale.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/locale.ML Tue Oct 04 19:01:37 2005 +0200
@@ -32,15 +32,15 @@
signature LOCALE =
sig
- type context = Proof.context
+ type context (*= Proof.context*)
datatype ('typ, 'term, 'fact) elem =
Fixes of (string * 'typ option * mixfix option) list |
Constrains of (string * 'typ) list |
Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
- type element = (string, string, thmref) elem
- type element_i = (typ, term, thm list) elem
+ type element (*= (string, string, thmref) elem*)
+ type element_i (*= (typ, term, thm list) elem*)
datatype expr =
Locale of string |
Rename of expr * (string * mixfix option) option list |
@@ -859,7 +859,7 @@
| unify_elemss _ [] [elems] = [elems]
| unify_elemss ctxt fixed_parms elemss =
let
- val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
+ val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
fun inst ((((name, ps), mode), elems), env) =
(((name, map (apsnd (Option.map (inst_type env))) ps),
map_mode (map (inst_thm ctxt env)) mode),
@@ -873,7 +873,7 @@
| unify_elemss' _ [] [elems] [] = [elems]
| unify_elemss' ctxt fixed_parms elemss c_parms =
let
- val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss @ map single c_parms);
+ val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms);
fun inst ((((name, ps), (ps', mode)), elems), env) =
(((name, map (apsnd (Option.map (inst_type env))) ps),
(ps', mode)),
@@ -1997,7 +1997,7 @@
val import = prep_expr thy raw_import;
val extraTs = foldr Term.add_term_tfrees [] exts' \\
- foldr Term.add_typ_tfrees [] (map #2 parms);
+ foldr Term.add_typ_tfrees [] (map snd parms);
val _ = if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^ quote bname);
--- a/src/Pure/Isar/method.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/method.ML Tue Oct 04 19:01:37 2005 +0200
@@ -149,11 +149,11 @@
(* datatype method *)
-datatype method = Method of thm list -> RuleCases.tactic;
+datatype method = Meth of thm list -> RuleCases.tactic;
-fun apply (Method m) = m;
+fun apply (Meth m) = m;
-val RAW_METHOD_CASES = Method;
+val RAW_METHOD_CASES = Meth;
fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
--- a/src/Pure/Isar/outer_parse.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML Tue Oct 04 19:01:37 2005 +0200
@@ -303,7 +303,7 @@
fun thm_name s = name -- opt_attribs --| $$$ s;
fun opt_thm_name s =
- Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);;
+ Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);
val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
--- a/src/Pure/Isar/proof.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 04 19:01:37 2005 +0200
@@ -7,8 +7,8 @@
signature PROOF =
sig
- type context = Context.proof
- type method = Method.method
+ type context (*= Context.proof*)
+ type method (*= Method.method*)
type state
exception STATE of string * state
val init: context -> state
--- a/src/Pure/Isar/proof_context.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Oct 04 19:01:37 2005 +0200
@@ -9,7 +9,7 @@
signature PROOF_CONTEXT =
sig
- type context = Context.proof
+ type context (*= Context.proof*)
type exporter
exception CONTEXT of string * context
val theory_of: context -> theory
--- a/src/Pure/Isar/proof_display.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Oct 04 19:01:37 2005 +0200
@@ -45,7 +45,7 @@
fun name_results "" res = res
| name_results name res =
let
- val n = length (List.concat (map #2 res));
+ val n = length (List.concat (map snd res));
fun name_res (a, ths) i =
let
val m = length ths;
@@ -57,7 +57,7 @@
((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
end;
- in #1 (fold_map name_res res 1) end;
+ in fst (fold_map name_res res 1) end;
in
--- a/src/Pure/Thy/thy_info.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/Thy/thy_info.ML Tue Oct 04 19:01:37 2005 +0200
@@ -364,7 +364,7 @@
val thy = if not really then SOME (get_theory name) else NONE;
val result =
- if current andalso forall #1 parent_results then true
+ if current andalso forall fst parent_results then true
else
((case new_deps of
SOME deps => change_thys (update_node name (map base_of_path parents) (deps, thy))
--- a/src/Pure/axclass.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/axclass.ML Tue Oct 04 19:01:37 2005 +0200
@@ -192,7 +192,7 @@
if null (term_tfrees ax) then
Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
else map_term_tfrees (K (aT [class])) ax;
- val abs_axms = map (abs_axm o #2) axms;
+ val abs_axms = map (abs_axm o snd) axms;
fun axm_sort (name, ax) =
(case term_tfrees ax of
--- a/src/Pure/context.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/context.ML Tue Oct 04 19:01:37 2005 +0200
@@ -314,7 +314,8 @@
fun create_thy name self id ids iids data ancestry history =
let
- val intermediate = #version history > 0;
+ val {version, name = _, intermediates = _} = history;
+ val intermediate = version > 0;
val (ids', iids') = check_insert intermediate id (ids, iids);
val id' = (serial (), name);
val _ = check_insert intermediate id' (ids', iids');
--- a/src/Pure/library.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/library.ML Tue Oct 04 19:01:37 2005 +0200
@@ -1165,7 +1165,7 @@
fun frequency xs =
let
val sum = foldl op + (0, map fst xs);
- fun pick n ((k, x) :: xs) =
+ fun pick n ((k: int, x) :: xs) =
if n <= k then x else pick (n - k) xs
in pick (random_range 1 sum) xs end;
--- a/src/Pure/meta_simplifier.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/meta_simplifier.ML Tue Oct 04 19:01:37 2005 +0200
@@ -296,8 +296,8 @@
val prcs = Net.entries procs |>
map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
|> partition_eq (eq_snd (op =))
- |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
- |> Library.sort_wrt #1;
+ |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps))
+ |> Library.sort_wrt fst;
in
[Pretty.big_list "simplification rules:" (pretty_thms smps),
Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
@@ -595,7 +595,7 @@
raise SIMPLIFIER ("Congruence must start with a constant", thm);
val (alist, _) = congs;
val alist2 = List.filter (fn (x, _) => x <> a) alist;
- val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}) =>
+ val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}: cong) =>
if is_full_cong thm then NONE else SOME a);
in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
@@ -692,7 +692,7 @@
fun ss delloop name = ss |>
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
- let val loop_tacs' = filter_out (equal name o #1) loop_tacs in
+ let val loop_tacs' = filter_out (equal name o fst) loop_tacs in
if length loop_tacs <> length loop_tacs' then ()
else warning ("No such looper in simpset: " ^ quote name);
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs', solvers)
--- a/src/Pure/pattern.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/pattern.ML Tue Oct 04 19:01:37 2005 +0200
@@ -444,12 +444,12 @@
(* Does pat match a subterm of obj? *)
fun matches_subterm thy (pat,obj) =
let fun msub(bounds,obj) = matches thy (pat,obj) orelse
- case obj of
+ (case obj of
Abs(x,T,t) => let val y = variant bounds x
val f = Free(":" ^ y,T)
in msub(x::bounds,subst_bound(f,t)) end
| s$t => msub(bounds,s) orelse msub(bounds,t)
- | _ => false
+ | _ => false)
in msub([],obj) end;
fun first_order(Abs(_,_,t)) = first_order t
--- a/src/Pure/proofterm.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/proofterm.ML Tue Oct 04 19:01:37 2005 +0200
@@ -15,8 +15,8 @@
PBound of int
| Abst of string * typ option * proof
| AbsP of string * term option * proof
- | op % of proof * term option
- | op %% of proof * proof
+ | % of proof * term option
+ | %% of proof * proof
| Hyp of term
| PThm of (string * (string * string list) list) * proof * term * typ list option
| PAxm of string * term * typ list option
--- a/src/Pure/sorts.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/sorts.ML Tue Oct 04 19:01:37 2005 +0200
@@ -240,7 +240,7 @@
witn_types path ts (solved_failed, S)
else
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
- if forall isSome ws then
+ if forall is_some ws then
let val w = (Type (t, map (#1 o valOf) ws), S)
in ((w :: solved', failed'), SOME w) end
else witn_types path ts ((solved', failed'), S)
--- a/src/Pure/term.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/term.ML Tue Oct 04 19:01:37 2005 +0200
@@ -27,7 +27,7 @@
Var of indexname * typ |
Bound of int |
Abs of string * typ * term |
- op $ of term * term
+ $ of term * term
exception TYPE of string * typ list * term list
exception TERM of string * term list
val dummyT: typ
--- a/src/Pure/type.ML Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/type.ML Tue Oct 04 19:01:37 2005 +0200
@@ -110,10 +110,10 @@
fun build_tsig (classes, default, types, arities) =
let
val log_types =
- Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (#2 types) []
- |> Library.sort (Library.int_ord o pairself #2) |> map #1;
+ Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
+ |> Library.sort (Library.int_ord o pairself snd) |> map fst;
val witness =
- (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
+ (case Sorts.witness_sorts (snd classes, arities) log_types [] [Graph.keys (snd classes)] of
[w] => SOME w | _ => NONE);
in make_tsig (classes, default, types, arities, log_types, witness) end;
@@ -488,7 +488,7 @@
fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
let
fun prep (t, Ss, S) =
- (case Symtab.lookup (#2 types) t of
+ (case Symtab.lookup (snd types) t of
SOME (LogicalType n, _) =>
if length Ss = n then
(t, map (cert_sort tsig) Ss, cert_sort tsig S)
@@ -498,7 +498,7 @@
| NONE => error (undecl_type t));
val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
- val arities' = fold (insert_arities pp (#2 classes)) ars arities;
+ val arities' = fold (insert_arities pp (snd classes)) ars arities;
in (classes, default, types, arities') end);
fun rebuild_arities pp classes arities =