# HG changeset patch
# User berghofe
# Date 1217868982 -7200
# Node ID d657036e26c56d4f67e0501fce3f0b0e1a28279a
# Parent  50a67d1977d7e95253966318a0b02093d1040108
- corrected bogus comment for function inst_conj_all
- tuned function obtain_fresh_name

diff -r 50a67d1977d7 -r d657036e26c5 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Aug 04 18:24:27 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Aug 04 18:56:22 2008 +0200
@@ -29,8 +29,6 @@
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
-val finite_Un = thm "finite_Un";
-val supp_prod = thm "supp_prod";
 val fresh_prod = thm "fresh_prod";
 
 val perm_bool = mk_meta_eq (thm "perm_bool");
@@ -83,9 +81,9 @@
 
 (*********************************************************************)
 (* maps  R ... & (ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t))  *)
-(* or    ALL pi_1 ... pi_n. P (pi_1 o ... o pi_n o t)                *)
-(* to    R ... & id (ALL z. (pi_1 o ... o pi_n o t))                 *)
-(* or    id (ALL z. (pi_1 o ... o pi_n o t))                         *)
+(* or    ALL pi_1 ... pi_n z. P z (pi_1 o ... o pi_n o t)            *)
+(* to    R ... & id (ALL z. P z (pi_1 o ... o pi_n o t))             *)
+(* or    id (ALL z. P z (pi_1 o ... o pi_n o t))                     *)
 (*                                                                   *)
 (* where "id" protects the subformula from simplification            *)
 (*********************************************************************)
@@ -291,7 +289,7 @@
 
     fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
       let
-        (** protect terms to avoid that supp_prod interferes with   **)
+        (** protect terms to avoid that fresh_prod interferes with  **)
         (** pairs used in introduction rules of inductive predicate **)
         fun protect t =
           let val T = fastype_of t in Const ("Fun.id", T --> T) $ t end;
@@ -302,7 +300,7 @@
                 Bound 0 $ p)))
           (fn _ => EVERY
             [resolve_tac exists_fresh' 1,
-             simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
+             resolve_tac fs_atoms 1]);
         val (([cx], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,