--- a/Nominal/Nominal2.thy	Tue Jun 28 14:45:30 2011 +0900
+++ b/Nominal/Nominal2.thy	Wed Jun 29 00:48:50 2011 +0100
@@ -218,7 +218,7 @@
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
   val _ = trace_msg (K "Defining raw fv- and bn-functions...")
-  val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
+  val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_inducts, lthy3a) =
     define_raw_bns raw_dt_names raw_dts raw_bn_funs raw_bn_eqs 
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     
@@ -235,19 +235,22 @@
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
     
+  val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct))
+  val _ = tracing ("alpha_intros\n" ^ cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_intros))
+
   val alpha_tys = map (domain_type o fastype_of) alpha_trms  
 
   val _ = trace_msg (K "Proving distinct theorems...")
   val alpha_distincts = 
-    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
+    raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
 
   val _ = trace_msg (K "Proving eq-iff theorems...")
   val alpha_eq_iff = 
-    mk_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
+    raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
     
   val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")
   val raw_bn_eqvt = 
-    raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_defs @ raw_perm_simps) lthy4
+    raw_prove_eqvt raw_bns raw_bn_inducts (raw_bn_defs @ raw_perm_simps) lthy4
     
   (* noting the raw_bn_eqvt lemmas in a temprorary theory *)
   val lthy_tmp = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_bn_eqvt) lthy4)
@@ -288,6 +291,8 @@
   val alpha_bn_imp_thms = 
     raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 
 
+  val _ = tracing ("alpha_bn_imp_thms:\n" ^ cat_lines (map (Syntax.string_of_term lthy5 o prop_of) alpha_bn_imp_thms))
+
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
     raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
@@ -381,7 +386,8 @@
   val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
     prod.cases} 
 
-  val ((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), lthyA) = 
+  val (((((((qdistincts, qeq_iffs), qfv_defs), qbn_defs), qperm_simps), qfv_qbn_eqvts), qbn_inducts), 
+    lthyA) = 
     lthy9a    
     |> lift_thms qtys [] alpha_distincts  
     ||>> lift_thms qtys eq_iff_simps alpha_eq_iff       
@@ -389,6 +395,7 @@
     ||>> lift_thms qtys [] raw_bn_defs
     ||>> lift_thms qtys [] raw_perm_simps
     ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
+    ||>> lift_thms qtys [] raw_bn_inducts
 
   val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = 
     lthyA 
@@ -399,7 +406,7 @@
     ||>> lift_thms qtys [] raw_perm_bn_simps
     ||>> lift_thms qtys [] alpha_refl_thms
 
-  val qinducts = Project_Rule.projections lthyA qinduct
+  val qinducts = Project_Rule.projections lthyB qinduct
 
   val _ = trace_msg (K "Proving supp lemmas and fs-instances...")
   val qsupports_thms =
@@ -470,8 +477,9 @@
      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
+     ||>> Local_Theory.note ((thms_suffix "bn_inducts", []), qbn_inducts) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
-     ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
+     ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", [eqvt_attr]), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size", [simp_attr]), qsize_simps)
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", [case_names_attr]), [qinduct])