--- a/Nominal/NewParser.thy	Fri Jul 30 00:40:32 2010 +0100
+++ b/Nominal/NewParser.thy	Sat Jul 31 01:24:39 2010 +0100
@@ -391,10 +391,12 @@
       (Local_Theory.restore lthy_tmp)
     else raise TEST lthy4
 
-  val size_eqvt = 
+  val raw_size_eqvt = 
     if get_STEPS lthy > 8
     then raw_prove_eqvt raw_size_trms raw_induct_thms (raw_size_thms @ raw_perm_simps) 
       (Local_Theory.restore lthy_tmp)
+      |> map (rewrite_rule @{thms permute_nat_def[THEN eq_reflection]})
+      |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
@@ -501,7 +503,9 @@
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
      ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), size_eqvt)
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
+     ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
+     ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
   
   val _ = 
     if get_STEPS lthy > 17