diff -r 29ebbe56f450 -r 428d9cb9a243 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Aug 17 06:50:49 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 07:11:45 2010 +0800
@@ -375,15 +375,15 @@
 
   (* proving equivariance lemmas for bns, fvs, size and alpha *)
   val _ = warning "Proving equivariance";
-  val bn_eqvt = 
+  val raw_bn_eqvt = 
     if get_STEPS lthy > 6
     then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4
     else raise TEST lthy4
 
-  (* noting the bn_eqvt lemmas in a temprorary theory *)
-  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), bn_eqvt) lthy4)
+  (* noting the raw_bn_eqvt lemmas in a temprorary theory *)
+  val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_bn_eqvt) lthy4)
 
-  val fv_eqvt = 
+  val raw_fv_eqvt = 
     if get_STEPS lthy > 7
     then raw_prove_eqvt (raw_fvs @ raw_fv_bns) raw_fv_bns_induct (raw_fv_defs @ raw_perm_simps) 
       (Local_Theory.restore lthy_tmp)
@@ -397,7 +397,7 @@
       |> map (fn thm => thm RS @{thm sym})
     else raise TEST lthy4
  
-  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), fv_eqvt) lthy_tmp)
+  val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attrib]), raw_fv_eqvt) lthy_tmp)
 
   val (alpha_eqvt, lthy6) =
     if get_STEPS lthy > 9
@@ -539,6 +539,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 "alpha_equivp"}, []), alpha_equivp_thms)
+     ||>> Local_Theory.note ((@{binding "fv_eqvt"}, []), raw_fv_eqvt) 
+     ||>> Local_Theory.note ((@{binding "bn_eqvt"}, []), raw_bn_eqvt)      
+     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)      
 
   val _ = 
     if get_STEPS lthy > 20
@@ -636,7 +639,7 @@
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
   val q_dis = map (lift_thm qtys lthy18) alpha_distincts;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm qtys lthy19) (bn_eqvt @ fv_eqvt);
+  val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";