src/HOL/Nominal/nominal_package.ML

       end
   | perm_simproc' thy ss _ = NONE;
 
 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 =
   ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule

                        resolve_tac final 1
                      end) context1 1) (constrs ~~ constrs')) (descr'' ~~ ndescr)))
       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);
 
     val induct_aux' = Thm.instantiate ([],