modernized theory setup;
authorwenzelm
Fri Apr 25 23:29:54 2014 +0200 (2014-04-25)
changeset 56732da3fefcb43c3
parent 56731 326e8a7ea287
child 56733 f7700146678d
modernized theory setup;
src/HOL/Record.thy
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Record.thy	Fri Apr 25 22:10:03 2014 +0200
     1.2 +++ b/src/HOL/Record.thy	Fri Apr 25 23:29:54 2014 +0200
     1.3 @@ -454,7 +454,7 @@
     1.4  
     1.5  subsection {* Record package *}
     1.6  
     1.7 -ML_file "Tools/record.ML" setup Record.setup
     1.8 +ML_file "Tools/record.ML"
     1.9  
    1.10  hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd
    1.11    iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons
     2.1 --- a/src/HOL/Tools/record.ML	Fri Apr 25 22:10:03 2014 +0200
     2.2 +++ b/src/HOL/Tools/record.ML	Fri Apr 25 23:29:54 2014 +0200
     2.3 @@ -50,7 +50,6 @@
     2.4    val updateN: string
     2.5    val ext_typeN: string
     2.6    val extN: string
     2.7 -  val setup: theory -> theory
     2.8  end;
     2.9  
    2.10  
    2.11 @@ -734,12 +733,14 @@
    2.12  
    2.13  in
    2.14  
    2.15 -val parse_translation =
    2.16 - [(@{syntax_const "_record_update"}, K record_update_tr),
    2.17 -  (@{syntax_const "_record"}, record_tr),
    2.18 -  (@{syntax_const "_record_scheme"}, record_scheme_tr),
    2.19 -  (@{syntax_const "_record_type"}, record_type_tr),
    2.20 -  (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)];
    2.21 +val _ =
    2.22 +  Theory.setup
    2.23 +   (Sign.parse_translation
    2.24 +     [(@{syntax_const "_record_update"}, K record_update_tr),
    2.25 +      (@{syntax_const "_record"}, record_tr),
    2.26 +      (@{syntax_const "_record_scheme"}, record_scheme_tr),
    2.27 +      (@{syntax_const "_record_type"}, record_type_tr),
    2.28 +      (@{syntax_const "_record_type_scheme"}, record_type_scheme_tr)]);
    2.29  
    2.30  end;
    2.31  
    2.32 @@ -1430,6 +1431,10 @@
    2.33      else no_tac
    2.34    end);
    2.35  
    2.36 +val _ =
    2.37 +  Theory.setup
    2.38 +    (map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]));
    2.39 +
    2.40  
    2.41  (* wrapper *)
    2.42  
    2.43 @@ -2312,13 +2317,6 @@
    2.44  end;
    2.45  
    2.46  
    2.47 -(* setup theory *)
    2.48 -
    2.49 -val setup =
    2.50 -  Sign.parse_translation parse_translation #>
    2.51 -  map_theory_simpset (fn ctxt => ctxt addsimprocs [simproc, upd_simproc, eq_simproc]);
    2.52 -
    2.53 -
    2.54  (* outer syntax *)
    2.55  
    2.56  val _ =