1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 26 16:25:25 2010 +0200
1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Aug 26 16:34:10 2010 +0200
1.3 @@ -730,9 +730,7 @@
1.4 type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
1.5 val empty = Symtab.empty;
1.6 val extend = I;
1.7 - val merge = Symtab.merge ((K true)
1.8 - : ((mode * (compilation_funs -> typ -> term)) list *
1.9 - (mode * (compilation_funs -> typ -> term)) list -> bool));
1.10 + fun merge data : T = Symtab.merge (K true) data;
1.11 );
1.12
1.13 fun alternative_compilation_of_global thy pred_name mode =
2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Aug 26 16:25:25 2010 +0200
2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Aug 26 16:34:10 2010 +0200
2.3 @@ -18,8 +18,7 @@
2.4 structure Specialisations = Theory_Data
2.5 (
2.6 type T = (term * term) Item_Net.T;
2.7 - val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
2.8 - (single o fst);
2.9 + val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
2.10 val extend = I;
2.11 val merge = Item_Net.merge;
2.12 )
3.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Aug 26 16:25:25 2010 +0200
3.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Aug 26 16:34:10 2010 +0200
3.3 @@ -56,10 +56,12 @@
3.4 type maps_info = {mapfun: string, relmap: string}
3.5
3.6 structure MapsData = Theory_Data
3.7 - (type T = maps_info Symtab.table
3.8 - val empty = Symtab.empty
3.9 - val extend = I
3.10 - fun merge data = Symtab.merge (K true) data)
3.11 +(
3.12 + type T = maps_info Symtab.table
3.13 + val empty = Symtab.empty
3.14 + val extend = I
3.15 + fun merge data = Symtab.merge (K true) data
3.16 +)
3.17
3.18 fun maps_defined thy s =
3.19 Symtab.defined (MapsData.get thy) s
3.20 @@ -120,10 +122,12 @@
3.21 type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
3.22
3.23 structure QuotData = Theory_Data
3.24 - (type T = quotdata_info Symtab.table
3.25 - val empty = Symtab.empty
3.26 - val extend = I
3.27 - fun merge data = Symtab.merge (K true) data)
3.28 +(
3.29 + type T = quotdata_info Symtab.table
3.30 + val empty = Symtab.empty
3.31 + val extend = I
3.32 + fun merge data = Symtab.merge (K true) data
3.33 +)
3.34
3.35 fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
3.36 {qtyp = Morphism.typ phi qtyp,
3.37 @@ -174,10 +178,12 @@
3.38 for example given "nat fset" we need to find "'a fset";
3.39 but overloaded constants share the same name *)
3.40 structure QConstsData = Theory_Data
3.41 - (type T = (qconsts_info list) Symtab.table
3.42 - val empty = Symtab.empty
3.43 - val extend = I
3.44 - val merge = Symtab.merge_list qconsts_info_eq)
3.45 +(
3.46 + type T = qconsts_info list Symtab.table
3.47 + val empty = Symtab.empty
3.48 + val extend = I
3.49 + val merge = Symtab.merge_list qconsts_info_eq
3.50 +)
3.51
3.52 fun transform_qconsts phi {qconst, rconst, def} =
3.53 {qconst = Morphism.term phi qconst,
4.1 --- a/src/Tools/Code/code_simp.ML Thu Aug 26 16:25:25 2010 +0200
4.2 +++ b/src/Tools/Code/code_simp.ML Thu Aug 26 16:34:10 2010 +0200
4.3 @@ -37,7 +37,8 @@
4.4
4.5 (* dedicated simpset *)
4.6
4.7 -structure Simpset = Theory_Data (
4.8 +structure Simpset = Theory_Data
4.9 +(
4.10 type T = simpset;
4.11 val empty = empty_ss;
4.12 fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
5.1 --- a/src/Tools/quickcheck.ML Thu Aug 26 16:25:25 2010 +0200
5.2 +++ b/src/Tools/quickcheck.ML Thu Aug 26 16:34:10 2010 +0200
5.3 @@ -78,27 +78,32 @@
5.4
5.5 datatype test_params = Test_Params of
5.6 { size: int, iterations: int, default_type: typ list, no_assms: bool,
5.7 - expect : expectation, report: bool, quiet : bool};
5.8 + expect : expectation, report: bool, quiet : bool};
5.9
5.10 fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
5.11 ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
5.12 +
5.13 fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
5.14 Test_Params { size = size, iterations = iterations, default_type = default_type,
5.15 - no_assms = no_assms, expect = expect, report = report, quiet = quiet };
5.16 + no_assms = no_assms, expect = expect, report = report, quiet = quiet };
5.17 +
5.18 fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
5.19 make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
5.20 -fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
5.21 - no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
5.22 +
5.23 +fun merge_test_params
5.24 + (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
5.25 + no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
5.26 Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
5.27 - no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
5.28 + no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
5.29 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
5.30 ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
5.31 ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
5.32
5.33 structure Data = Theory_Data
5.34 (
5.35 - type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
5.36 - * test_params;
5.37 + type T =
5.38 + (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
5.39 + * test_params;
5.40 val empty = ([], Test_Params
5.41 { size = 10, iterations = 100, default_type = [], no_assms = false,
5.42 expect = No_Expectation, report = false, quiet = false});