assert Pure equations for theorem references; avoid dynamic reference to fact
authorhaftmann
Sat Sep 03 17:32:35 2011 +0200 (2011-09-03 ago)
changeset 44685f5bc7d9d0d74
parent 44684 8dde3352d5c4
child 44686 364716401696
assert Pure equations for theorem references; avoid dynamic reference to fact
src/HOL/Nominal/nominal_datatype.ML
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 17:32:34 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 17:32:35 2011 +0200
     1.3 @@ -155,9 +155,9 @@
     1.4  val supp_prod = @{thm supp_prod};
     1.5  val fresh_prod = @{thm fresh_prod};
     1.6  val supports_fresh = @{thm supports_fresh};
     1.7 -val supports_def = @{thm Nominal.supports_def};
     1.8 -val fresh_def = @{thm fresh_def};
     1.9 -val supp_def = @{thm supp_def};
    1.10 +val supports_def = Simpdata.mk_eq @{thm Nominal.supports_def};
    1.11 +val fresh_def = Simpdata.mk_eq @{thm fresh_def};
    1.12 +val supp_def = Simpdata.mk_eq @{thm supp_def};
    1.13  val rev_simps = @{thms rev.simps};
    1.14  val app_simps = @{thms append.simps};
    1.15  val at_fin_set_supp = @{thm at_fin_set_supp};
    1.16 @@ -306,7 +306,7 @@
    1.17      val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
    1.18  
    1.19      val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
    1.20 -    val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
    1.21 +    val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
    1.22  
    1.23      val unfolded_perm_eq_thms =
    1.24        if length descr = length new_type_names then []