simplification/standardization of some theory data;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 16:25:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Aug 26 16:34:10 2010 +0200
@@ -730,9 +730,7 @@
   type T = (mode * (compilation_funs -> typ -> term)) list Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  val merge = Symtab.merge ((K true)
-    : ((mode * (compilation_funs -> typ -> term)) list *
-      (mode * (compilation_funs -> typ -> term)) list -> bool));
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 fun alternative_compilation_of_global thy pred_name mode =

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Aug 26 16:25:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML	Thu Aug 26 16:34:10 2010 +0200
@@ -18,8 +18,7 @@
 structure Specialisations = Theory_Data
 (
   type T = (term * term) Item_Net.T;
-  val empty = Item_Net.init ((op aconv o pairself fst) : (term * term) * (term * term) -> bool)
-    (single o fst);
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val extend = I;
   val merge = Item_Net.merge;
 )

--- 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/Code/code_simp.ML	Thu Aug 26 16:25:25 2010 +0200
+++ b/src/Tools/Code/code_simp.ML	Thu Aug 26 16:34:10 2010 +0200
@@ -37,7 +37,8 @@
 
 (* dedicated simpset *)
 
-structure Simpset = Theory_Data (
+structure Simpset = Theory_Data
+(
   type T = simpset;
   val empty = empty_ss;
   fun extend ss = MetaSimplifier.inherit_context empty_ss ss;

--- 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});