--- a/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100
@@ -169,7 +169,7 @@
({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
set_arities = set_arities1, pred_arities = pred_arities1},
{to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
- set_arities = set_arities2, pred_arities = pred_arities2}) =
+ set_arities = set_arities2, pred_arities = pred_arities2}) : T =
{to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
--- a/src/HOL/Tools/lin_arith.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Jan 01 14:23:39 2009 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Tools/lin_arith.ML
- ID: $Id$
- Author: Tjark Weber and Tobias Nipkow
+ Author: Tjark Weber and Tobias Nipkow, TU Muenchen
HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
*)
@@ -99,8 +98,9 @@
tactics: arith_tactic list};
val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
val extend = I;
- fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
- {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) =
+ fun merge _
+ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
+ {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
{splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
discrete = Library.merge (op =) (discrete1, discrete2),
--- a/src/HOL/Tools/refute.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Tools/refute.ML Thu Jan 01 14:23:39 2009 +0100
@@ -389,11 +389,6 @@
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
- (* (''a * 'b) list -> ''a -> 'b *)
-
- fun lookup xs key =
- Option.valOf (AList.lookup (op =) xs key);
-
(* ------------------------------------------------------------------------- *)
(* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *)
(* ('Term.typ'), given type parameters for the data type's type *)
@@ -405,12 +400,12 @@
fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
(* replace a 'DtTFree' variable by the associated type *)
- lookup typ_assoc (DatatypeAux.DtTFree a)
+ the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
| typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
Type (s, map (typ_of_dtyp descr typ_assoc) ds)
| typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
let
- val (s, ds, _) = lookup descr i
+ val (s, ds, _) = the (AList.lookup (op =) descr i)
in
Type (s, map (typ_of_dtyp descr typ_assoc) ds)
end;
@@ -850,14 +845,14 @@
| Const ("The", T) =>
let
val ax = specialize_type thy ("The", T)
- (lookup axioms "HOL.the_eq_trivial")
+ (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
in
collect_this_axiom ("HOL.the_eq_trivial", ax) axs
end
| Const ("Hilbert_Choice.Eps", T) =>
let
val ax = specialize_type thy ("Hilbert_Choice.Eps", T)
- (lookup axioms "Hilbert_Choice.someI")
+ (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
in
collect_this_axiom ("Hilbert_Choice.someI", ax) axs
end
@@ -955,7 +950,7 @@
let
val index = #index info
val descr = #descr info
- val (_, typs, _) = lookup descr index
+ val (_, typs, _) = the (AList.lookup (op =) descr index)
val typ_assoc = typs ~~ Ts
(* sanity check: every element in 'dtyps' must be a *)
(* 'DtTFree' *)
@@ -981,7 +976,7 @@
acc (* prevent infinite recursion *)
else
let
- val (_, dtyps, dconstrs) = lookup descr i
+ val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)
(* if the current type is a recursive IDT (i.e. a depth *)
(* is required), add it to 'acc' *)
val acc_dT = if Library.exists (fn (_, ds) =>
@@ -1165,7 +1160,7 @@
let
val index = #index info
val descr = #descr info
- val (_, _, constrs) = lookup descr index
+ val (_, _, constrs) = the (AList.lookup (op =) descr index)
in
(* recursive datatype? *)
Library.exists (fn (_, ds) =>
@@ -1657,7 +1652,7 @@
fun interpret_groundtype () =
let
(* the model must specify a size for ground types *)
- val size = (if T = Term.propT then 2 else lookup typs T)
+ val size = if T = Term.propT then 2 else the (AList.lookup (op =) typs T)
val next = next_idx+size
(* check if 'maxvars' is large enough *)
val _ = (if next-1>maxvars andalso maxvars>0 then
@@ -2020,7 +2015,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = lookup descr index
+ val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = if Library.exists (fn d =>
@@ -2144,7 +2139,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = lookup descr index
+ val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = if Library.exists (fn d =>
@@ -2204,7 +2199,7 @@
let
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = lookup descr index
+ val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
val typ_assoc = dtyps ~~ Ts'
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = if Library.exists (fn d =>
@@ -2400,7 +2395,7 @@
(* the index of some mutually recursive IDT *)
val index = #index info
val descr = #descr info
- val (_, dtyps, _) = lookup descr index
+ val (_, dtyps, _) = the (AList.lookup (op =) descr index)
(* sanity check: we assume that the order of constructors *)
(* in 'descr' is the same as the order of *)
(* corresponding parameters, otherwise the *)
@@ -2459,7 +2454,7 @@
end
| DatatypeAux.DtRec i =>
let
- val (_, ds, _) = lookup descr i
+ val (_, ds, _) = the (AList.lookup (op =) descr i)
val (_, Ts) = dest_Type T
in
rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
@@ -2473,10 +2468,10 @@
raise REFUTE ("IDT_recursion_interpreter",
"different type associations for the same dtyp"))
(* (DatatypeAux.dtyp * Term.typ) list *)
- val typ_assoc = List.filter
+ val typ_assoc = filter
(fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
(rec_typ_assoc []
- (#2 (lookup descr idt_index) ~~ (snd o dest_Type) IDT))
+ (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
(* sanity check: typ_assoc must associate types to the *)
(* elements of 'dtyps' (and only to those) *)
val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
@@ -2600,7 +2595,7 @@
SOME args => (n, args)
| NONE => get_cargs_rec (n+1, xs))
in
- get_cargs_rec (0, lookup mc_intrs idx)
+ get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
end
(* computes one entry in 'REC_OPERATORS', and recursively *)
(* all entries needed for it, where 'idx' gives the *)
@@ -2608,7 +2603,7 @@
(* int -> int -> interpretation *)
fun compute_array_entry idx elem =
let
- val arr = lookup REC_OPERATORS idx
+ val arr = the (AList.lookup (op =) REC_OPERATORS idx)
val (flag, intr) = Array.sub (arr, elem)
in
if flag then
@@ -2622,7 +2617,7 @@
val (c, args) = get_cargs idx elem
(* find the indices of the constructor's /recursive/ *)
(* arguments *)
- val (_, _, constrs) = lookup descr idx
+ val (_, _, constrs) = the (AList.lookup (op =) descr idx)
val (_, dtyps) = List.nth (constrs, c)
val rec_dtyps_args = List.filter
(DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
@@ -2674,7 +2669,7 @@
result
end
end
- val idt_size = Array.length (lookup REC_OPERATORS idt_index)
+ val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
(* sanity check: the size of 'IDT' should be 'idt_size' *)
val _ = if idt_size <> size_of_type thy (typs, []) IDT then
raise REFUTE ("IDT_recursion_interpreter",
@@ -2973,8 +2968,8 @@
(* nat -> nat -> interpretation *)
fun append m n =
let
- val (len_m, off_m) = lookup lenoff_lists m
- val (len_n, off_n) = lookup lenoff_lists n
+ val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
+ val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
val len_elem = len_m + len_n
val off_elem = off_m * power (size_elem, len_n) + off_n
in
@@ -3262,7 +3257,7 @@
val (typs, _) = model
val index = #index info
val descr = #descr info
- val (_, dtyps, constrs) = lookup descr index
+ val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
val typ_assoc = dtyps ~~ Ts
(* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
val _ = if Library.exists (fn d =>
--- a/src/Pure/Isar/code_unit.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML Thu Jan 01 14:23:39 2009 +0100
@@ -229,7 +229,7 @@
val empty = ([], []);
val copy = I;
val extend = I;
- fun merge _ ((alias1, classes1), (alias2, classes2)) =
+ fun merge _ ((alias1, classes1), (alias2, classes2)) : T =
(Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2),
Library.merge (op =) (classes1, classes2));
);
--- a/src/Pure/Isar/expression.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/Pure/Isar/expression.ML Thu Jan 01 14:23:39 2009 +0100
@@ -74,7 +74,7 @@
end;
fun match_bind (n, b) = (n = Binding.base_name b);
- fun parm_eq ((b1, mx1), (b2, mx2)) =
+ fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
(* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
(Binding.base_name b1 = Binding.base_name b2) andalso
(if mx1 = mx2 then true
--- a/src/Pure/Isar/new_locale.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/Pure/Isar/new_locale.ML Thu Jan 01 14:23:39 2009 +0100
@@ -115,17 +115,17 @@
val extend = I;
fun join_locales _
- (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
- Loc {decls = (decls1', decls2'), notes = notes',
- dependencies = dependencies', ...}) =
- let fun s_merge x = merge (eq_snd (op =)) x in
- Loc {parameters = parameters,
- spec = spec,
- decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')),
- notes = s_merge (notes, notes'),
- dependencies = s_merge (dependencies, dependencies')
- }
- end;
+ (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
+ Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
+ Loc {
+ parameters = parameters,
+ spec = spec,
+ decls =
+ (merge (eq_snd op =) (decls1, decls1'),
+ merge (eq_snd op =) (decls2, decls2')),
+ notes = merge (eq_snd op =) (notes, notes'),
+ dependencies = merge (eq_snd op =) (dependencies, dependencies')};
+
fun merge _ = NameSpace.join_tables join_locales;
);
@@ -197,7 +197,7 @@
val empty = ([] : identifiers);
-fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
+fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
local
@@ -221,7 +221,7 @@
Ready _ => NONE |
ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
)));
-
+
fun get_global_idents thy =
let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
@@ -331,7 +331,7 @@
in
ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
ProofContext.add_assms_i Assumption.assume_export assms' |> snd
- end
+ end
| init_local_elem (Defines defs) ctxt =
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
@@ -376,7 +376,7 @@
in
Pretty.big_list "locale elements:"
(activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
- (empty, []) |> snd |> rev |>
+ (empty, []) |> snd |> rev |>
map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
end
@@ -393,7 +393,7 @@
(* registrations, in reverse order of declaration *)
val empty = [];
val extend = I;
- fun merge _ = Library.merge (eq_snd (op =));
+ fun merge _ data : T = Library.merge (eq_snd op =) data;
(* FIXME consolidate with dependencies, consider one data slot only *)
);
--- a/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100
@@ -1695,7 +1695,7 @@
val empty = NameSpace.empty_table;
val copy = I;
val extend = I;
- fun merge _ oracles = NameSpace.merge_tables (op =) oracles
+ fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles
handle Symtab.DUP dup => err_dup_ora dup;
);
--- a/src/Tools/value.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/Tools/value.ML Thu Jan 01 14:23:39 2009 +0100
@@ -20,7 +20,7 @@
val empty = [];
val copy = I;
val extend = I;
- fun merge pp = AList.merge (op =) (K true);
+ fun merge _ data = AList.merge (op =) (K true) data;
)
val add_evaluator = Evaluator.map o AList.update (op =);