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