--- 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"
(******************************************************)
--- 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);
--- 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);