# HG changeset patch
# User paulson
# Date 909834236 -3600
# Node ID 95ac0bf10518896b443509b9c0bfefdfec952672
# Parent  7559f116cb100ca0271316782bb0b5fc75ca5f1d
no need for int_0

diff -r 7559f116cb10 -r 95ac0bf10518 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Sat Oct 31 12:42:34 1998 +0100
+++ b/src/HOL/UNITY/Lift.ML	Sat Oct 31 12:43:56 1998 +0100
@@ -247,7 +247,7 @@
 (** LEVEL 6 **)
 by (ALLGOALS (asm_simp_tac (simpset() addsimps 
 			    [zle_def] @ metric_simps @ zcompare_rls)));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps int_0::zadd_ac)));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
 qed "E_thm12b";
 
 (*lift_4*)
@@ -288,7 +288,7 @@
 by Auto_tac;
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (ALLGOALS
-    (asm_simp_tac (simpset() addsimps [int_0, zle_def] @ 
+    (asm_simp_tac (simpset() addsimps [zle_def] @ 
 		                      metric_simps @ zcompare_rls)));
 (** LEVEL 5 **)
 by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);