diff -r ba7955d211c4 -r 76646fc8b1bf src/HOL/NumberTheory/Chinese.ML
--- a/src/HOL/NumberTheory/Chinese.ML	Mon Oct 09 12:25:10 2000 +0200
+++ b/src/HOL/NumberTheory/Chinese.ML	Mon Oct 09 14:10:55 2000 +0200
@@ -210,7 +210,7 @@
 by (asm_full_simp_tac (simpset() addsimps zmult_ac) 7);
 by (rewtac xilin_sol_def);
 by (Asm_simp_tac 7);
-by (rtac (ex1_implies_ex RS ex_someI) 7);
+by (rtac (ex1_implies_ex RS someI_ex) 7);
 by (rtac unique_xi_sol 7);
 by (rtac funprod_zdvd 4);
 by (rewtac m_cond_def);