--- 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);