diff -r 326e8a7ea287 -r da3fefcb43c3 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Apr 25 22:10:03 2014 +0200
+++ b/src/HOL/Tools/record.ML	Fri Apr 25 23:29:54 2014 +0200
@@ -50,7 +50,6 @@
   val updateN: string
   val ext_typeN: string
   val extN: string
-  val setup: theory -> theory
 end;
 
 
@@ -734,12 +733,14 @@
 
 in
 
-val parse_translation =
- [(@{syntax_const "_record_update"}, K record_update_tr),
-  (@{syntax_const "_record"}, record_tr),
-  (@{syntax_const "_record_scheme"}, record_scheme_tr),
-  (@{syntax_const "_record_type"}, record_type_tr),
-  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
+val _ =
+  Theory.setup
+   (Sign.parse_translation
+     [(@{syntax_const "_record_update"}, K record_update_tr),
+      (@{syntax_const "_record"}, record_tr),
+      (@{syntax_const "_record_scheme"}, record_scheme_tr),
+      (@{syntax_const "_record_type"}, record_type_tr),
+      (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]);
 
 end;
 
@@ -1430,6 +1431,10 @@
     else no_tac
   end);
 
+val _ =
+  Theory.setup
+    (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
+
 
 (* wrapper *)
 
@@ -2312,13 +2317,6 @@
 end;
 
 
-(* setup theory *)
-
-val setup =
-  Sign.parse_translation parse_translation #>
-  map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
-
-
 (* outer syntax *)
 
 val _ =