# HG changeset patch
# User wenzelm
# Date 1213631679 -7200
# Node ID 4f7976a6ffc3d6130cb44dc67059661d18ac858a
# Parent  184d7601c062d022f24b150343a90b64cbaae573
allE_Nil: only one copy, proven in regular theory source;

diff -r 184d7601c062 -r 4f7976a6ffc3 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Mon Jun 16 17:54:38 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Mon Jun 16 17:54:39 2008 +0200
@@ -3528,6 +3528,9 @@
 
 (************************************************)
 (* main file for constructing nominal datatypes *)
+lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
+  using assms ..
+
 use "nominal_package.ML"
 
 (******************************************************)
diff -r 184d7601c062 -r 4f7976a6ffc3 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Mon Jun 16 17:54:38 2008 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Jun 16 17:54:39 2008 +0200
@@ -48,8 +48,6 @@
          then SOME perm_bool else NONE
      | _ => NONE);
 
-val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
-
 fun transp ([] :: _) = []
   | transp xs = map hd xs :: transp (map tl xs);
 
@@ -401,7 +399,7 @@
         in
           cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
           REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
-            etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN
+            etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
             asm_full_simp_tac (simpset_of thy) 1)
         end);
 
diff -r 184d7601c062 -r 4f7976a6ffc3 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Mon Jun 16 17:54:38 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Jun 16 17:54:39 2008 +0200
@@ -155,8 +155,6 @@
 val perm_simproc =
   Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
 
-val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE;
-
 val meta_spec = thm "meta_spec";
 
 fun projections rule =
@@ -1349,7 +1347,7 @@
       in
         EVERY
           [cut_facts_tac [th] 1,
-           REPEAT (eresolve_tac [conjE, allE_Nil] 1),
+           REPEAT (eresolve_tac [conjE, @{thm allE_Nil}] 1),
            REPEAT (etac allE 1),
            REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)]
       end);