--- a/Nominal/nominal_dt_alpha.ML	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Wed Nov 10 13:46:21 2010 +0000
@@ -445,7 +445,7 @@
 
 fun cases_tac intros ctxt =
   let
-    val prod_simps = @{thms split_conv prod_alpha_def prod_rel.simps}
+    val prod_simps = @{thms split_conv prod_alpha_def prod_rel_def}
 
     val unbound_tac = REPEAT o (etac @{thm conjE}) THEN' atac  
 
@@ -493,7 +493,7 @@
         in
           resolve_tac prems' 1
         end) ctxt
-    val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel.simps alphas}
+    val prod_simps = @{thms split_conv permute_prod.simps prod_alpha_def prod_rel_def alphas}
   in
     EVERY' 
       [ etac exi_neg,
@@ -543,7 +543,7 @@
 
 fun non_trivial_cases_tac pred_names intros ctxt = 
   let
-    val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel.simps}
+    val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
   in
     resolve_tac intros
     THEN_ALL_NEW (asm_simp_tac HOL_basic_ss THEN' 
@@ -596,8 +596,8 @@
 
 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
   let
-    val refl' = map (fold_rule @{thms reflp_def} o atomize) refl
-    val symm' = map (fold_rule @{thms symp_def} o atomize) symm
+    val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl
+    val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm
     val trans' = map (fold_rule [transp_def'] o atomize) trans
 
     fun prep_goal t = 
@@ -671,7 +671,7 @@
 
     val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys 
   
-    val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps 
+    val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel_def 
       permute_prod_def prod.cases prod.recs})
 
     val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss
@@ -685,7 +685,7 @@
 fun raw_constr_rsp_tac alpha_intros simps = 
   let
     val pre_ss = HOL_ss addsimps @{thms fun_rel_def}
-    val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps 
+    val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel_def 
       prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps
   in
     asm_full_simp_tac pre_ss
@@ -754,7 +754,7 @@
 (* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma
-  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}
+  "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)}
 
 fun mk_funs_rsp thm = 
   thm
@@ -765,7 +765,7 @@
 
 val permute_rsp = @{lemma 
   "(!x y p. R x y --> R (permute p x) (permute p y)) 
-     ==> ((op =) ===> R ===> R) permute permute"  by simp}
+     ==> ((op =) ===> R ===> R) permute permute"  by (simp add: fun_rel_def)}
 
 fun mk_alpha_permute_rsp thm = 
   thm