--- a/src/HOL/Lambda/Eta.ML Thu Oct 08 11:59:17 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML Fri Oct 09 11:10:59 1998 +0200
@@ -44,7 +44,7 @@
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];
@@ -119,7 +119,7 @@
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];
@@ -163,7 +163,7 @@
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);