# HG changeset patch
# User haftmann
# Date 1315063955 -7200
# Node ID f5bc7d9d0d74a9e1f02eb649c7c7b15c0ebae64e
# Parent  8dde3352d5c425df250035b270fe5bb2558d0dc2
assert Pure equations for theorem references; avoid dynamic reference to fact

diff -r 8dde3352d5c4 -r f5bc7d9d0d74 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 17:32:34 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Sep 03 17:32:35 2011 +0200
@@ -155,9 +155,9 @@
 val supp_prod = @{thm supp_prod};
 val fresh_prod = @{thm fresh_prod};
 val supports_fresh = @{thm supports_fresh};
-val supports_def = @{thm Nominal.supports_def};
-val fresh_def = @{thm fresh_def};
-val supp_def = @{thm supp_def};
+val supports_def = Simpdata.mk_eq @{thm Nominal.supports_def};
+val fresh_def = Simpdata.mk_eq @{thm fresh_def};
+val supp_def = Simpdata.mk_eq @{thm supp_def};
 val rev_simps = @{thms rev.simps};
 val app_simps = @{thms append.simps};
 val at_fin_set_supp = @{thm at_fin_set_supp};
@@ -306,7 +306,7 @@
     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
 
     val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
-    val perm_fun_def = Global_Theory.get_thm thy2 "perm_fun_def";
+    val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
 
     val unfolded_perm_eq_thms =
       if length descr = length new_type_names then []