--- 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 _ =