diff -r 35c570891a3a -r 98236fbd8aa6 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Fri Dec 03 13:51:07 2010 +0000
@@ -593,14 +593,20 @@
 
 (** proves the equivp predicate for all alphas **)
 
+val reflp_def' = 
+  @{lemma "reflp R == !x. R x x" by (simp add: reflp_def refl_on_def)}
+
+val symp_def' =
+  @{lemma "symp R == !x y . R x y --> R y x" by (simp add: symp_def sym_def)}
+
 val transp_def' =
   @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
-    by (rule eq_reflection, auto simp add: transp_def)}
+    by (rule eq_reflection, auto simp add: trans_def transp_def)}
 
 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
   let
-    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 refl' = map (fold_rule [reflp_def'] o atomize) refl
+    val symm' = map (fold_rule [symp_def'] o atomize) symm
     val trans' = map (fold_rule [transp_def'] o atomize) trans
 
     fun prep_goal t =