diff -r 66ae73fd66c0 -r 29ebbe56f450 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue Aug 17 06:39:27 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 06:50:49 2010 +0800
@@ -341,7 +341,7 @@
 
   (* definition of raw fv_functions *)
   val _ = warning "Definition of raw fv-functions";
-  val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+  val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
     then raw_bn_decls raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) lthy3
@@ -377,7 +377,7 @@
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
-    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_simps) lthy4
+    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 *)
@@ -439,7 +439,7 @@
   
   (* respectfulness proofs *)
   val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-    raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+    raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
   val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
@@ -534,6 +534,7 @@
      ||>> Local_Theory.note ((@{binding "eq_iff"}, []), alpha_eq_iff)
      ||>> Local_Theory.note ((@{binding "eq_iff_simps"}, []), alpha_eq_iff_simps) 
      ||>> Local_Theory.note ((@{binding "fv_defs"}, []), raw_fv_defs) 
+     ||>> Local_Theory.note ((@{binding "bn_defs"}, []), raw_bn_defs) 
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
@@ -554,7 +555,7 @@
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
   val bns = raw_bns ~~ bn_nos;
 
-  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_defs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -622,7 +623,7 @@
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm qtys lthy15) raw_fv_defs;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
+  val q_bn = map (lift_thm qtys lthy16) raw_bn_defs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)