# HG changeset patch
# User nipkow
# Date 889605236 -3600
# Node ID b72dd6b2ba56d0e08989fd887baefc04296e9b85
# Parent  b820f57a2323f4cd0b566b5b53d3dde9368a2486
New Asm_full_simp_tac led to a loop.

diff -r b820f57a2323 -r b72dd6b2ba56 src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Tue Mar 10 20:24:28 1998 +0100
+++ b/src/HOL/ex/Primes.ML	Wed Mar 11 09:33:56 1998 +0100
@@ -79,10 +79,10 @@
 goal thy "k * gcd(m,n) = gcd(k*m, k*n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "k=0" 1);
-by (case_tac "n=0" 2);
-by (ALLGOALS 
-    (asm_full_simp_tac (simpset() addsimps
-       [mod_less_divisor, mod_geq, mod_mult_distrib2])));
+ by(Asm_full_simp_tac 1);
+by (case_tac "n=0" 1);
+ by(Asm_full_simp_tac 1);
+by(asm_full_simp_tac (simpset() addsimps [mod_geq, mod_mult_distrib2]) 1);
 qed "gcd_mult_distrib2";
 
 (*This theorem leads immediately to a proof of the uniqueness of factorization.