# HG changeset patch
# User narboux
# Date 1177072235 -7200
# Node ID 49d7818e6161c95c61c7ae78288e6caa0daf5096
# Parent  8b3131eeb509643188e1f6beecb39eeb816c92ff
modify fresh_fun_simp to ease debugging

diff -r 8b3131eeb509 -r 49d7818e6161 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Apr 20 13:30:51 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Apr 20 14:30:35 2007 +0200
@@ -9,6 +9,14 @@
 (* First some functions that could be
  in the library *)
 
+(* A tactical which implements Coq's T;[a,b,c] *)
+
+infix 1 THENL
+
+fun THENL (tac,tacs) =
+ tac THEN
+  (EVERY (map  (fn (tac,i) => tac i) (rev tacs ~~ (length tacs downto 1))))
+
 fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
   let
     val thy = theory_of_thm st;
@@ -133,17 +141,20 @@
     val atom_basename = Sign.base_name atom_name;
     val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
     val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
+    fun tac_a i = 
+      res_inst_tac_term' [(x,Bound n)] false exI i THEN
+      asm_full_simp_tac ss' i                      THEN 
+      NominalPermeq.fresh_guess_tac HOL_ss i;
   in
-  (generate_fresh_tac atom_name i               THEN
-   subst_outer_tac ctx fresh_fun_app i          THEN
-   rtac pt_name_inst i                          THEN
-   rtac at_name_inst i                          THEN
-   NominalPermeq.finite_guess_tac HOL_ss i      THEN
-   auto_tac (HOL_cs , HOL_ss)                   THEN
-   NominalPermeq.fresh_guess_tac HOL_ss (i+1)   THEN
-   res_inst_tac_term' [(x,Bound n)] false exI i THEN
-   asm_full_simp_tac ss' i                      THEN
-   NominalPermeq.fresh_guess_tac HOL_ss i) thm 
+  (generate_fresh_tac atom_name i      THEN 
+   subst_outer_tac ctx fresh_fun_app i THENL 
+   [rtac pt_name_inst,
+    rtac at_name_inst, 
+    (fn i => TRY (NominalPermeq.finite_guess_tac HOL_ss i)),   
+    tac_a, 
+    (fn i => TRY (NominalPermeq.fresh_guess_tac  HOL_ss i)),
+    (fn i => auto_tac (HOL_cs, HOL_ss)) 
+]) thm 
   end
   end