# HG changeset patch
# User hoelzl
# Date 1354179560 -3600
# Node ID e79a8341dd6b7ca017633c6cf27d4b90b06c4f4c
# Parent  902ccccf2efa8c46f2338894c06b0fd1a3e3e50e
make SML/NJ happy (give names for all fields in a record)

diff -r 902ccccf2efa -r e79a8341dd6b src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 28 19:19:39 2012 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Nov 29 09:59:20 2012 +0100
@@ -1545,11 +1545,12 @@
     dest_thms = Thm.full_rules,
     app_thms = Thm.full_rules};
   val extend = I;
-  fun merge (t1, t2) = {
-    concrete_thms = Item_Net.merge (#concrete_thms t1, #concrete_thms t2),
-    generic_thms = Item_Net.merge (#generic_thms t1, #generic_thms t2),
-    dest_thms = Item_Net.merge (#dest_thms t1, #dest_thms t2),
-    app_thms = Item_Net.merge (#app_thms t1, #app_thms t2) };
+  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
+      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
+    concrete_thms = Item_Net.merge (ct1, ct2),
+    generic_thms = Item_Net.merge (gt1, gt2),
+    dest_thms = Item_Net.merge (dt1, dt2),
+    app_thms = Item_Net.merge (at1, at2) };
 );
 
 val debug =
@@ -1731,7 +1732,7 @@
 fun simproc ss redex = let
     val ctxt = Simplifier.the_context ss;
     val t = HOLogic.mk_Trueprop (term_of redex);
-    fun tac {context = ctxt, ...} =
+    fun tac {context = ctxt, prems = _ } =
       SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
   in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;