minor tweaks for Poplog/ML;
authorwenzelm
Tue Oct 04 19:01:37 2005 +0200 (2005-10-04)
changeset 17756d4a35f82fbb4
parent 17755 b0cd55afead1
child 17757 87a9b1d48e25
minor tweaks for Poplog/ML;
src/Pure/General/name_space.ML
src/Pure/General/pretty.ML
src/Pure/General/stack.ML
src/Pure/General/symbol.ML
src/Pure/General/xml.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/isar_output.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Thy/thy_info.ML
src/Pure/axclass.ML
src/Pure/context.ML
src/Pure/library.ML
src/Pure/meta_simplifier.ML
src/Pure/pattern.ML
src/Pure/proofterm.ML
src/Pure/sorts.ML
src/Pure/term.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Oct 04 16:47:40 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Oct 04 19:01:37 2005 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4    val custom_accesses: (string list -> string list list) -> naming -> naming
     1.5    val set_policy: (string -> bstring -> string) * (string list -> string list list) ->
     1.6      naming -> naming
     1.7 -  type 'a table = T * 'a Symtab.table
     1.8 +  type 'a table (*= T * 'a Symtab.table*)
     1.9    val empty_table: 'a table
    1.10    val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
    1.11    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
     2.1 --- a/src/Pure/General/pretty.ML	Tue Oct 04 16:47:40 2005 +0200
     2.2 +++ b/src/Pure/General/pretty.ML	Tue Oct 04 19:01:37 2005 +0200
     2.3 @@ -78,7 +78,7 @@
     2.4  datatype T =
     2.5    Block of T list * int * int |         (*body, indentation, length*)
     2.6    String of string * int |              (*text, length*)
     2.7 -  Break of bool * int;                  (*mandatory flag, width if not taken*);
     2.8 +  Break of bool * int;                  (*mandatory flag, width if not taken*)
     2.9  
    2.10  
    2.11  
    2.12 @@ -88,19 +88,21 @@
    2.13  val add_indent = Buffer.add o output_spaces;
    2.14  fun set_indent wd = Buffer.empty |> add_indent wd;
    2.15  
    2.16 -val empty =
    2.17 +type text = {tx: Buffer.T, ind: Buffer.T, pos: int, nl: int};
    2.18 +
    2.19 +val empty: text =
    2.20   {tx = Buffer.empty,
    2.21    ind = Buffer.empty,
    2.22    pos = 0,
    2.23    nl = 0};
    2.24  
    2.25 -fun newline {tx, ind, pos, nl} =
    2.26 +fun newline {tx, ind, pos, nl} : text =
    2.27   {tx = Buffer.add (Output.output "\n") tx,
    2.28    ind = Buffer.empty,
    2.29    pos = 0,
    2.30    nl = nl + 1};
    2.31  
    2.32 -fun string (s, len) {tx, ind, pos: int, nl} =
    2.33 +fun string (s, len) {tx, ind, pos: int, nl} : text =
    2.34   {tx = Buffer.add s tx,
    2.35    ind = Buffer.add s ind,
    2.36    pos = pos + len,
    2.37 @@ -108,7 +110,7 @@
    2.38  
    2.39  fun blanks wd = string (output_spaces wd, wd);
    2.40  
    2.41 -fun indentation (buf, len) {tx, ind, pos, nl} =
    2.42 +fun indentation (buf, len) {tx, ind, pos, nl} : text =
    2.43    let val s = Buffer.content buf in
    2.44     {tx = Buffer.add (Output.indent (s, len)) tx,
    2.45      ind = Buffer.add s ind,
    2.46 @@ -160,7 +162,7 @@
    2.47              val block' =
    2.48                if pos' < emergencypos then (ind |> add_indent indent, pos')
    2.49                else (set_indent pos'', pos'');
    2.50 -            val btext = format (bes, block', breakdist (es, after)) text;
    2.51 +            val btext: text = format (bes, block', breakdist (es, after)) text;
    2.52              (*if this block was broken then force the next break*)
    2.53              val es2 = if nl < #nl btext then forcenext es else es;
    2.54            in format (es2, block, after) btext end
     3.1 --- a/src/Pure/General/stack.ML	Tue Oct 04 16:47:40 2005 +0200
     3.2 +++ b/src/Pure/General/stack.ML	Tue Oct 04 19:01:37 2005 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  signature STACK =
     3.6  sig
     3.7 -  type 'a T = 'a * 'a list
     3.8 +  type 'a T (*= 'a * 'a list*)
     3.9    val level: 'a T -> int
    3.10    val init: 'a -> 'a T
    3.11    val top: 'a T -> 'a
     4.1 --- a/src/Pure/General/symbol.ML	Tue Oct 04 16:47:40 2005 +0200
     4.2 +++ b/src/Pure/General/symbol.ML	Tue Oct 04 19:01:37 2005 +0200
     4.3 @@ -132,7 +132,7 @@
     4.4    | is_ascii_quasi _ = false;
     4.5  
     4.6  val is_ascii_blank =
     4.7 -  fn " " => true | "\t" => true | "\r" => true | "\n" => true | "\^L" => true
     4.8 +  fn " " => true | "\t" => true | "\n" => true | "\^L" => true | "\^M" => true
     4.9      | _ => false;
    4.10  
    4.11  
    4.12 @@ -389,8 +389,8 @@
    4.13  local
    4.14  
    4.15  val scan_encoded_newline =
    4.16 -  $$ "\r" -- $$ "\n" >> K "\n" ||
    4.17 -  $$ "\r" >> K "\n" ||
    4.18 +  $$ "\^M" -- $$ "\n" >> K "\n" ||
    4.19 +  $$ "\^M" >> K "\n" ||
    4.20    $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
    4.21  
    4.22  val scan_raw =
    4.23 @@ -422,7 +422,7 @@
    4.24  
    4.25  fun no_explode [] = true
    4.26    | no_explode ("\\" :: "<" :: _) = false
    4.27 -  | no_explode ("\r" :: _) = false
    4.28 +  | no_explode ("\^M" :: _) = false
    4.29    | no_explode (_ :: cs) = no_explode cs;
    4.30  
    4.31  fun sym_explode str =
     5.1 --- a/src/Pure/General/xml.ML	Tue Oct 04 16:47:40 2005 +0200
     5.2 +++ b/src/Pure/General/xml.ML	Tue Oct 04 19:01:37 2005 +0200
     5.3 @@ -47,11 +47,11 @@
     5.4    | encode "\"" = "&quot;"
     5.5    | encode c = c;
     5.6  
     5.7 -fun encode_charref c = "&#"^Int.toString (Char.ord c)^ ";"
     5.8 +fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
     5.9  
    5.10  val text = Library.translate_string encode
    5.11  
    5.12 -val text_charref = implode o (map encode_charref) o String.explode
    5.13 +val text_charref = translate_string encode_charref;
    5.14  
    5.15  val cdata = enclose "<![CDATA[" "]]>\n"
    5.16  
     6.1 --- a/src/Pure/Isar/attrib.ML	Tue Oct 04 16:47:40 2005 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Tue Oct 04 19:01:37 2005 +0200
     6.3 @@ -282,7 +282,7 @@
     6.4      val ctxt = init context;
     6.5      val thy = ProofContext.theory_of ctxt;
     6.6  
     6.7 -    val (type_insts, term_insts) = List.partition (is_tvar o #1) (map #2 mixed_insts);
     6.8 +    val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
     6.9      val internal_insts = term_insts |> List.mapPartial
    6.10        (fn (xi, Args.Term t) => SOME (xi, t)
    6.11        | (_, Args.Name _) => NONE
     7.1 --- a/src/Pure/Isar/find_theorems.ML	Tue Oct 04 16:47:40 2005 +0200
     7.2 +++ b/src/Pure/Isar/find_theorems.ML	Tue Oct 04 19:01:37 2005 +0200
     7.3 @@ -218,7 +218,7 @@
     7.4  
     7.5  fun opt_not x = if isSome x then NONE else SOME (0, 0);
     7.6  
     7.7 -fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y)
     7.8 +fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
     7.9   |  opt_add _ _ = NONE;
    7.10  
    7.11  in
     8.1 --- a/src/Pure/Isar/isar_output.ML	Tue Oct 04 16:47:40 2005 +0200
     8.2 +++ b/src/Pure/Isar/isar_output.ML	Tue Oct 04 19:01:37 2005 +0200
     8.3 @@ -206,22 +206,21 @@
     8.4  (* command spans *)
     8.5  
     8.6  type command = string * Position.T * string list;   (*name, position, tags*)
     8.7 -type tok = token * string * int;         (*token, markup flag, meta-comment depth*)
     8.8 -type source = tok list;
     8.9 +type source = (token * (string * int)) list;        (*token, markup flag, meta-comment depth*)
    8.10  
    8.11  datatype span = Span of command * (source * source * source * source) * bool;
    8.12  
    8.13  fun make_span cmd src =
    8.14    let
    8.15 -    fun take_newline ((tok: tok) :: toks) =
    8.16 -          if newline_token (#1 tok) then ([tok], toks, true)
    8.17 +    fun take_newline (tok :: toks) =
    8.18 +          if newline_token (fst tok) then ([tok], toks, true)
    8.19            else ([], tok :: toks, false)
    8.20        | take_newline [] = ([], [], false);
    8.21      val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) =
    8.22        src
    8.23 -      |> take_prefix (improper_token o #1)
    8.24 -      ||>> take_suffix (improper_token o #1)
    8.25 -      ||>> take_prefix (comment_token o #1)
    8.26 +      |> take_prefix (improper_token o fst)
    8.27 +      ||>> take_suffix (improper_token o fst)
    8.28 +      ||>> take_prefix (comment_token o fst)
    8.29        ||> take_newline;
    8.30    in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end;
    8.31  
    8.32 @@ -246,7 +245,7 @@
    8.33  fun present_span lex default_tags span state state'
    8.34      (tag_stack, active_tag, newline, buffer, present_cont) =
    8.35    let
    8.36 -    val present = fold (fn (tok, flag, 0) =>
    8.37 +    val present = fold (fn (tok, (flag, 0)) =>
    8.38          Buffer.add (output_token lex state' tok)
    8.39          #> Buffer.add flag
    8.40        | _ => I);
    8.41 @@ -332,7 +331,7 @@
    8.42      (* tokens *)
    8.43  
    8.44      val ignored = Scan.state --| ignore
    8.45 -      >> (fn d => (NONE, (NoToken, "", d)));
    8.46 +      >> (fn d => (NONE, (NoToken, ("", d))));
    8.47  
    8.48      fun markup mark mk flag = Scan.peek (fn d =>
    8.49        improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
    8.50 @@ -340,21 +339,21 @@
    8.51        P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
    8.52        >> (fn (((tok, pos), tags), txt) =>
    8.53          let val name = T.val_of tok
    8.54 -        in (SOME (name, pos, tags), (mk (name, txt), flag, d)) end));
    8.55 +        in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
    8.56  
    8.57      val command = Scan.peek (fn d =>
    8.58        P.position (Scan.one (T.is_kind T.Command)) --
    8.59        Scan.repeat tag
    8.60        >> (fn ((tok, pos), tags) =>
    8.61          let val name = T.val_of tok
    8.62 -        in (SOME (name, pos, tags), (BasicToken tok, Latex.markup_false, d)) end));
    8.63 +        in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    8.64  
    8.65      val cmt = Scan.peek (fn d =>
    8.66        P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
    8.67 -      >> (fn txt => (NONE, (MarkupToken ("cmt", txt), "", d))));
    8.68 +      >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
    8.69  
    8.70      val other = Scan.peek (fn d =>
    8.71 -       Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, "", d))));
    8.72 +       Scan.one T.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
    8.73  
    8.74      val token =
    8.75        ignored ||
    8.76 @@ -367,15 +366,15 @@
    8.77      (* spans *)
    8.78  
    8.79      val stopper =
    8.80 -      ((NONE, (BasicToken (#1 T.stopper), "", 0)),
    8.81 -        fn (_, (BasicToken x, _, _)) => #2 T.stopper x | _ => false);
    8.82 +      ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
    8.83 +        fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
    8.84  
    8.85 -    val cmd = Scan.one (is_some o #1);
    8.86 -    val non_cmd = Scan.one (is_none o #1 andf not o #2 stopper) >> #2;
    8.87 +    val cmd = Scan.one (is_some o fst);
    8.88 +    val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
    8.89  
    8.90 -    val comments = Scan.any (comment_token o #1 o #2);
    8.91 -    val blank = Scan.one (blank_token o #1 o #2);
    8.92 -    val newline = Scan.one (newline_token o #1 o #2);
    8.93 +    val comments = Scan.any (comment_token o fst o snd);
    8.94 +    val blank = Scan.one (blank_token o fst o snd);
    8.95 +    val newline = Scan.one (newline_token o fst o snd);
    8.96      val before_cmd =
    8.97        Scan.option (newline -- comments) --
    8.98        Scan.option (newline -- comments) --
    8.99 @@ -384,9 +383,9 @@
   8.100      val span =
   8.101        Scan.repeat non_cmd -- cmd --
   8.102          Scan.repeat (Scan.unless before_cmd non_cmd) --
   8.103 -        Scan.option (newline >> (single o #2))
   8.104 +        Scan.option (newline >> (single o snd))
   8.105        >> (fn (((toks1, (cmd, tok2)), toks3), tok4) =>
   8.106 -          make_span (the cmd) (toks1 @ tok2 :: toks3 @ the_default [] tok4));
   8.107 +          make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
   8.108  
   8.109      val spans =
   8.110        src
     9.1 --- a/src/Pure/Isar/locale.ML	Tue Oct 04 16:47:40 2005 +0200
     9.2 +++ b/src/Pure/Isar/locale.ML	Tue Oct 04 19:01:37 2005 +0200
     9.3 @@ -32,15 +32,15 @@
     9.4  
     9.5  signature LOCALE =
     9.6  sig
     9.7 -  type context = Proof.context
     9.8 +  type context (*= Proof.context*)
     9.9    datatype ('typ, 'term, 'fact) elem =
    9.10      Fixes of (string * 'typ option * mixfix option) list |
    9.11      Constrains of (string * 'typ) list |
    9.12      Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    9.13      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    9.14      Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
    9.15 -  type element = (string, string, thmref) elem
    9.16 -  type element_i = (typ, term, thm list) elem
    9.17 +  type element (*= (string, string, thmref) elem*)
    9.18 +  type element_i (*= (typ, term, thm list) elem*)
    9.19    datatype expr =
    9.20      Locale of string |
    9.21      Rename of expr * (string * mixfix option) option list |
    9.22 @@ -859,7 +859,7 @@
    9.23    | unify_elemss _ [] [elems] = [elems]
    9.24    | unify_elemss ctxt fixed_parms elemss =
    9.25        let
    9.26 -        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss);
    9.27 +        val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss);
    9.28          fun inst ((((name, ps), mode), elems), env) =
    9.29            (((name, map (apsnd (Option.map (inst_type env))) ps), 
    9.30                map_mode (map (inst_thm ctxt env)) mode),
    9.31 @@ -873,7 +873,7 @@
    9.32    | unify_elemss' _ [] [elems] [] = [elems]
    9.33    | unify_elemss' ctxt fixed_parms elemss c_parms =
    9.34        let
    9.35 -        val envs = unify_parms ctxt fixed_parms (map (#2 o #1 o #1) elemss @ map single c_parms);
    9.36 +        val envs = unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms);
    9.37          fun inst ((((name, ps), (ps', mode)), elems), env) =
    9.38            (((name, map (apsnd (Option.map (inst_type env))) ps),
    9.39                (ps', mode)),
    9.40 @@ -1997,7 +1997,7 @@
    9.41      val import = prep_expr thy raw_import;
    9.42  
    9.43      val extraTs = foldr Term.add_term_tfrees [] exts' \\
    9.44 -      foldr Term.add_typ_tfrees [] (map #2 parms);
    9.45 +      foldr Term.add_typ_tfrees [] (map snd parms);
    9.46      val _ = if null extraTs then ()
    9.47        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    9.48  
    10.1 --- a/src/Pure/Isar/method.ML	Tue Oct 04 16:47:40 2005 +0200
    10.2 +++ b/src/Pure/Isar/method.ML	Tue Oct 04 19:01:37 2005 +0200
    10.3 @@ -149,11 +149,11 @@
    10.4  
    10.5  (* datatype method *)
    10.6  
    10.7 -datatype method = Method of thm list -> RuleCases.tactic;
    10.8 +datatype method = Meth of thm list -> RuleCases.tactic;
    10.9  
   10.10 -fun apply (Method m) = m;
   10.11 +fun apply (Meth m) = m;
   10.12  
   10.13 -val RAW_METHOD_CASES = Method;
   10.14 +val RAW_METHOD_CASES = Meth;
   10.15  
   10.16  fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
   10.17  
    11.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Oct 04 16:47:40 2005 +0200
    11.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Oct 04 19:01:37 2005 +0200
    11.3 @@ -303,7 +303,7 @@
    11.4  
    11.5  fun thm_name s = name -- opt_attribs --| $$$ s;
    11.6  fun opt_thm_name s =
    11.7 -  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);;
    11.8 +  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);
    11.9  
   11.10  val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
   11.11  val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    12.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 04 16:47:40 2005 +0200
    12.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 04 19:01:37 2005 +0200
    12.3 @@ -7,8 +7,8 @@
    12.4  
    12.5  signature PROOF =
    12.6  sig
    12.7 -  type context = Context.proof
    12.8 -  type method = Method.method
    12.9 +  type context (*= Context.proof*)
   12.10 +  type method (*= Method.method*)
   12.11    type state
   12.12    exception STATE of string * state
   12.13    val init: context -> state
    13.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 04 16:47:40 2005 +0200
    13.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 04 19:01:37 2005 +0200
    13.3 @@ -9,7 +9,7 @@
    13.4  
    13.5  signature PROOF_CONTEXT =
    13.6  sig
    13.7 -  type context = Context.proof
    13.8 +  type context (*= Context.proof*)
    13.9    type exporter
   13.10    exception CONTEXT of string * context
   13.11    val theory_of: context -> theory
    14.1 --- a/src/Pure/Isar/proof_display.ML	Tue Oct 04 16:47:40 2005 +0200
    14.2 +++ b/src/Pure/Isar/proof_display.ML	Tue Oct 04 19:01:37 2005 +0200
    14.3 @@ -45,7 +45,7 @@
    14.4  fun name_results "" res = res
    14.5    | name_results name res =
    14.6        let
    14.7 -        val n = length (List.concat (map #2 res));
    14.8 +        val n = length (List.concat (map snd res));
    14.9          fun name_res (a, ths) i =
   14.10            let
   14.11              val m = length ths;
   14.12 @@ -57,7 +57,7 @@
   14.13                ((PureThy.string_of_thmref (NameSelection (name, [Single i])), ths), j)
   14.14              else ((PureThy.string_of_thmref (NameSelection (name, [FromTo (i, j - 1)])), ths), j)
   14.15            end;
   14.16 -      in #1 (fold_map name_res res 1) end;
   14.17 +      in fst (fold_map name_res res 1) end;
   14.18  
   14.19  in
   14.20  
    15.1 --- a/src/Pure/Thy/thy_info.ML	Tue Oct 04 16:47:40 2005 +0200
    15.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Oct 04 19:01:37 2005 +0200
    15.3 @@ -364,7 +364,7 @@
    15.4  
    15.5          val thy = if not really then SOME (get_theory name) else NONE;
    15.6          val result =
    15.7 -          if current andalso forall #1 parent_results then true
    15.8 +          if current andalso forall fst parent_results then true
    15.9            else
   15.10              ((case new_deps of
   15.11                SOME deps => change_thys (update_node name (map base_of_path parents) (deps, thy))
    16.1 --- a/src/Pure/axclass.ML	Tue Oct 04 16:47:40 2005 +0200
    16.2 +++ b/src/Pure/axclass.ML	Tue Oct 04 19:01:37 2005 +0200
    16.3 @@ -192,7 +192,7 @@
    16.4        if null (term_tfrees ax) then
    16.5          Logic.mk_implies (Logic.mk_inclass (aT [], class), ax)
    16.6        else map_term_tfrees (K (aT [class])) ax;
    16.7 -    val abs_axms = map (abs_axm o #2) axms;
    16.8 +    val abs_axms = map (abs_axm o snd) axms;
    16.9  
   16.10      fun axm_sort (name, ax) =
   16.11        (case term_tfrees ax of
    17.1 --- a/src/Pure/context.ML	Tue Oct 04 16:47:40 2005 +0200
    17.2 +++ b/src/Pure/context.ML	Tue Oct 04 19:01:37 2005 +0200
    17.3 @@ -314,7 +314,8 @@
    17.4  
    17.5  fun create_thy name self id ids iids data ancestry history =
    17.6    let
    17.7 -    val intermediate = #version history > 0;
    17.8 +    val {version, name = _, intermediates = _} = history;
    17.9 +    val intermediate = version > 0;
   17.10      val (ids', iids') = check_insert intermediate id (ids, iids);
   17.11      val id' = (serial (), name);
   17.12      val _ = check_insert intermediate id' (ids', iids');
    18.1 --- a/src/Pure/library.ML	Tue Oct 04 16:47:40 2005 +0200
    18.2 +++ b/src/Pure/library.ML	Tue Oct 04 19:01:37 2005 +0200
    18.3 @@ -1165,7 +1165,7 @@
    18.4  fun frequency xs =
    18.5    let
    18.6      val sum = foldl op + (0, map fst xs);
    18.7 -    fun pick n ((k, x) :: xs) =
    18.8 +    fun pick n ((k: int, x) :: xs) =
    18.9        if n <= k then x else pick (n - k) xs
   18.10    in pick (random_range 1 sum) xs end;
   18.11  
    19.1 --- a/src/Pure/meta_simplifier.ML	Tue Oct 04 16:47:40 2005 +0200
    19.2 +++ b/src/Pure/meta_simplifier.ML	Tue Oct 04 19:01:37 2005 +0200
    19.3 @@ -296,8 +296,8 @@
    19.4      val prcs = Net.entries procs |>
    19.5        map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
    19.6        |> partition_eq (eq_snd (op =))
    19.7 -      |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))
    19.8 -      |> Library.sort_wrt #1;
    19.9 +      |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps))
   19.10 +      |> Library.sort_wrt fst;
   19.11    in
   19.12      [Pretty.big_list "simplification rules:" (pretty_thms smps),
   19.13        Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
   19.14 @@ -595,7 +595,7 @@
   19.15          raise SIMPLIFIER ("Congruence must start with a constant", thm);
   19.16        val (alist, _) = congs;
   19.17        val alist2 = List.filter (fn (x, _) => x <> a) alist;
   19.18 -      val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}) =>
   19.19 +      val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}: cong) =>
   19.20          if is_full_cong thm then NONE else SOME a);
   19.21      in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
   19.22  
   19.23 @@ -692,7 +692,7 @@
   19.24  
   19.25  fun ss delloop name = ss |>
   19.26    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
   19.27 -    let val loop_tacs' = filter_out (equal name o #1) loop_tacs in
   19.28 +    let val loop_tacs' = filter_out (equal name o fst) loop_tacs in
   19.29        if length loop_tacs <> length loop_tacs' then ()
   19.30        else warning ("No such looper in simpset: " ^ quote name);
   19.31        (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs', solvers)
    20.1 --- a/src/Pure/pattern.ML	Tue Oct 04 16:47:40 2005 +0200
    20.2 +++ b/src/Pure/pattern.ML	Tue Oct 04 19:01:37 2005 +0200
    20.3 @@ -444,12 +444,12 @@
    20.4  (* Does pat match a subterm of obj? *)
    20.5  fun matches_subterm thy (pat,obj) =
    20.6    let fun msub(bounds,obj) = matches thy (pat,obj) orelse
    20.7 -            case obj of
    20.8 +            (case obj of
    20.9                Abs(x,T,t) => let val y = variant bounds x
   20.10                                  val f = Free(":" ^ y,T)
   20.11                              in msub(x::bounds,subst_bound(f,t)) end
   20.12              | s$t => msub(bounds,s) orelse msub(bounds,t)
   20.13 -            | _ => false
   20.14 +            | _ => false)
   20.15    in msub([],obj) end;
   20.16  
   20.17  fun first_order(Abs(_,_,t)) = first_order t
    21.1 --- a/src/Pure/proofterm.ML	Tue Oct 04 16:47:40 2005 +0200
    21.2 +++ b/src/Pure/proofterm.ML	Tue Oct 04 19:01:37 2005 +0200
    21.3 @@ -15,8 +15,8 @@
    21.4       PBound of int
    21.5     | Abst of string * typ option * proof
    21.6     | AbsP of string * term option * proof
    21.7 -   | op % of proof * term option
    21.8 -   | op %% of proof * proof
    21.9 +   | % of proof * term option
   21.10 +   | %% of proof * proof
   21.11     | Hyp of term
   21.12     | PThm of (string * (string * string list) list) * proof * term * typ list option
   21.13     | PAxm of string * term * typ list option
    22.1 --- a/src/Pure/sorts.ML	Tue Oct 04 16:47:40 2005 +0200
    22.2 +++ b/src/Pure/sorts.ML	Tue Oct 04 19:01:37 2005 +0200
    22.3 @@ -240,7 +240,7 @@
    22.4                  witn_types path ts (solved_failed, S)
    22.5                else
    22.6                  let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
    22.7 -                  if forall isSome ws then
    22.8 +                  if forall is_some ws then
    22.9                      let val w = (Type (t, map (#1 o valOf) ws), S)
   22.10                      in ((w :: solved', failed'), SOME w) end
   22.11                    else witn_types path ts ((solved', failed'), S)
    23.1 --- a/src/Pure/term.ML	Tue Oct 04 16:47:40 2005 +0200
    23.2 +++ b/src/Pure/term.ML	Tue Oct 04 19:01:37 2005 +0200
    23.3 @@ -27,7 +27,7 @@
    23.4      Var of indexname * typ |
    23.5      Bound of int |
    23.6      Abs of string * typ * term |
    23.7 -    op $ of term * term
    23.8 +    $ of term * term
    23.9    exception TYPE of string * typ list * term list
   23.10    exception TERM of string * term list
   23.11    val dummyT: typ
    24.1 --- a/src/Pure/type.ML	Tue Oct 04 16:47:40 2005 +0200
    24.2 +++ b/src/Pure/type.ML	Tue Oct 04 19:01:37 2005 +0200
    24.3 @@ -110,10 +110,10 @@
    24.4  fun build_tsig (classes, default, types, arities) =
    24.5    let
    24.6      val log_types =
    24.7 -      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (#2 types) []
    24.8 -      |> Library.sort (Library.int_ord o pairself #2) |> map #1;
    24.9 +      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
   24.10 +      |> Library.sort (Library.int_ord o pairself snd) |> map fst;
   24.11      val witness =
   24.12 -      (case Sorts.witness_sorts (#2 classes, arities) log_types [] [Graph.keys (#2 classes)] of
   24.13 +      (case Sorts.witness_sorts (snd classes, arities) log_types [] [Graph.keys (snd classes)] of
   24.14          [w] => SOME w | _ => NONE);
   24.15    in make_tsig (classes, default, types, arities, log_types, witness) end;
   24.16  
   24.17 @@ -488,7 +488,7 @@
   24.18  fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   24.19    let
   24.20      fun prep (t, Ss, S) =
   24.21 -      (case Symtab.lookup (#2 types) t of
   24.22 +      (case Symtab.lookup (snd types) t of
   24.23          SOME (LogicalType n, _) =>
   24.24            if length Ss = n then
   24.25              (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   24.26 @@ -498,7 +498,7 @@
   24.27        | NONE => error (undecl_type t));
   24.28  
   24.29      val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   24.30 -    val arities' = fold (insert_arities pp (#2 classes)) ars arities;
   24.31 +    val arities' = fold (insert_arities pp (snd classes)) ars arities;
   24.32    in (classes, default, types, arities') end);
   24.33  
   24.34  fun rebuild_arities pp classes arities =