src/HOL/Lambda/Eta.ML

 by (Asm_simp_tac 2);
 by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (simpset())) 2);
 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
                       addsplits [nat.split]) 1);
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (safe_tac (HOL_cs addSEs [linorder_neqE]));
 by (ALLGOALS trans_tac);
 qed "free_subst";
 Addsimps [free_subst];
 
 Goal "s -e> t ==> !i. free t i = free s i";

 AddIs [beta_subst];
 
 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
 by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
+by (safe_tac (HOL_cs addSEs [linorder_neqE]));
 by (ALLGOALS trans_tac);
 qed_spec_mp "subst_Var_Suc";
 Addsimps [subst_Var_Suc];
 
 Goal "s -e> t ==> (!i. lift s i -e> lift t i)";

 
 Goal "!i. (~free s i) = (? t. s = lift t i)";
 by (induct_tac "s" 1);
   by (Simp_tac 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
-   by (etac nat_neqE 1);
+   by (etac linorder_neqE 1);
     by (res_inst_tac [("x","Var nat")] exI 1);
     by (Asm_simp_tac 1);
    by (res_inst_tac [("x","Var(nat-1)")] exI 1);
    by (Asm_simp_tac 1);
   by (rtac notE 1);