--- a/src/HOL/Tools/Quotient/quotient_info.ML Thu Aug 26 16:25:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Thu Aug 26 16:34:10 2010 +0200
@@ -56,10 +56,12 @@
type maps_info = {mapfun: string, relmap: string}
structure MapsData = Theory_Data
- (type T = maps_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data)
+(
+ type T = maps_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
fun maps_defined thy s =
Symtab.defined (MapsData.get thy) s
@@ -120,10 +122,12 @@
type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
structure QuotData = Theory_Data
- (type T = quotdata_info Symtab.table
- val empty = Symtab.empty
- val extend = I
- fun merge data = Symtab.merge (K true) data)
+(
+ type T = quotdata_info Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+)
fun transform_quotdata phi {qtyp, rtyp, equiv_rel, equiv_thm} =
{qtyp = Morphism.typ phi qtyp,
@@ -174,10 +178,12 @@
for example given "nat fset" we need to find "'a fset";
but overloaded constants share the same name *)
structure QConstsData = Theory_Data
- (type T = (qconsts_info list) Symtab.table
- val empty = Symtab.empty
- val extend = I
- val merge = Symtab.merge_list qconsts_info_eq)
+(
+ type T = qconsts_info list Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ val merge = Symtab.merge_list qconsts_info_eq
+)
fun transform_qconsts phi {qconst, rconst, def} =
{qconst = Morphism.term phi qconst,
--- a/src/Tools/quickcheck.ML Thu Aug 26 16:25:25 2010 +0200
+++ b/src/Tools/quickcheck.ML Thu Aug 26 16:34:10 2010 +0200
@@ -78,27 +78,32 @@
datatype test_params = Test_Params of
{ size: int, iterations: int, default_type: typ list, no_assms: bool,
- expect : expectation, report: bool, quiet : bool};
+ expect : expectation, report: bool, quiet : bool};
fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
+
fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
Test_Params { size = size, iterations = iterations, default_type = default_type,
- no_assms = no_assms, expect = expect, report = report, quiet = quiet };
+ no_assms = no_assms, expect = expect, report = report, quiet = quiet };
+
fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
-fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
- no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
+
+fun merge_test_params
+ (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
+ no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
- no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
+ no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
structure Data = Theory_Data
(
- type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
- * test_params;
+ type T =
+ (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
+ * test_params;
val empty = ([], Test_Params
{ size = 10, iterations = 100, default_type = [], no_assms = false,
expect = No_Expectation, report = false, quiet = false});