diff -r a8ebcb368a15 -r e5fa8de0e4bd Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Jan 06 23:06:45 2011 +0000
+++ b/Nominal/Nominal2.thy	Fri Jan 07 02:30:00 2011 +0000
@@ -250,7 +250,7 @@
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
-    Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+    Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
 
   val _ = trace_msg (K "Proving equivalence of alpha...")
   val alpha_refl_thms =