# HG changeset patch
# User wenzelm
# Date 1398461394 -7200
# Node ID da3fefcb43c3c3199c418d59ce3cee7afc5a3948
# Parent  326e8a7ea287d9993ce946d16a1994c20b698188
modernized theory setup;

diff -r 326e8a7ea287 -r da3fefcb43c3 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Fri Apr 25 22:10:03 2014 +0200
+++ b/src/HOL/Record.thy	Fri Apr 25 23:29:54 2014 +0200
@@ -454,7 +454,7 @@
 
 subsection {* Record package *}
 
-ML_file "Tools/record.ML" setup Record.setup
+ML_file "Tools/record.ML"
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
   iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
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 _ =