--- a/Nominal/nominal_dt_supp.ML	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/nominal_dt_supp.ML	Mon Dec 06 16:35:42 2010 +0000
@@ -18,7 +18,7 @@
 
   val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list
   val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list ->
-    Proof.context -> thm list
+    thm list -> Proof.context -> thm list
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -204,7 +204,7 @@
     induct_prove qtys props qinduct (K ss_tac) ctxt
   end
 
-fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs ctxt =
+fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt =
   let 
     val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt
     val p = Free (p, @{typ perm})
@@ -218,12 +218,11 @@
 
     val props = map2 mk_goal qperm_bns alpha_bns
     val ss_tac = (K (print_tac "test")) THEN' 
-      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs))
+      asm_full_simp_tac (HOL_ss addsimps (@{thm id_def}::qperm_bn_simps @ qeq_iffs @ qalpha_refls))
   in
-    @{thms TrueI}
-    (*induct_prove qtys props qinduct (K ss_tac) ctxt'
+    induct_prove qtys props qinduct (K ss_tac) ctxt'
     |> ProofContext.export ctxt' ctxt
-    |> map (simplify (HOL_basic_ss addsimps @{thms id_def}))*)
+    |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) 
   end