--- a/Nominal/Nominal2.thy	Wed Jun 29 23:08:44 2011 +0100
+++ b/Nominal/Nominal2.thy	Thu Jun 30 02:19:59 2011 +0100
@@ -232,14 +232,9 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
     
   val _ = trace_msg (K "Defining alpha relations...")
-  val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) =
+  val (alpha_result, 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 = 
     raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names
@@ -267,7 +262,11 @@
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
   val alpha_eqvt =
-    Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+    let
+      val AlphaResult {alpha_trms, alpha_bn_trms, alpha_raw_induct, alpha_intros, ...} = alpha_result
+    in
+      Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_raw_induct alpha_intros lthy5
+    end
 
   val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
 
@@ -281,35 +280,27 @@
     raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms
 
   val _ = trace_msg (K "Proving alpha implies bn...")
-  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 alpha_bn_imp_thms = raw_prove_bn_imp lthy5 alpha_result
 
   val _ = trace_msg (K "Proving respectfulness...")
   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_defs @ raw_fv_defs) lthy5
+    raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) 
   
   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 
-      (raw_size_thms @ raw_size_eqvt) lthy5
+    raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
       |> map mk_funs_rsp
 
   val raw_constrs_rsp = 
-    raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
-      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 
+    raw_constrs_rsp lthy5 alpha_result (flat raw_constrs) (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
     
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
   val alpha_bn_rsp = 
-    raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp_thms alpha_bn_imp_thms
+    raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
 
-  val raw_perm_bn_rsp =
-    raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct 
-      alpha_intros raw_perm_bn_simps lthy5
+  val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
@@ -321,7 +312,11 @@
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+    let
+      val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result
+    in
+      define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+    end
 
   val qtys = map #qtyp qty_infos
   val qty_full_names = map (fst o dest_Type) qtys
@@ -341,7 +336,11 @@
     map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn)) bn_funs raw_fv_bns
 
   val qalpha_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+    let
+      val AlphaResult {alpha_bn_trms, ...} = alpha_result 
+    in
+      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn)) bn_funs  alpha_bn_trms
+    end
 
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
@@ -484,7 +483,6 @@
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
      ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
-     ||>> Local_Theory.note ((thms_suffix "raw_alpha", []), alpha_intros)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_simps", []), qperm_bn_simps)
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)