# HG changeset patch
# User paulson
# Date 806947525 -7200
# Node ID 653f33d8d79187f48efc1492122d4010017f8059
# Parent  230b9b4b783e5d25096e11a7b96b44bc7b8a02c1
changed AC_... to OrdQuant_...

diff -r 230b9b4b783e -r 653f33d8d791 src/ZF/AC/Transrec2.ML
--- a/src/ZF/AC/Transrec2.ML	Fri Jul 28 17:41:31 1995 +0200
+++ b/src/ZF/AC/Transrec2.ML	Fri Jul 28 18:05:25 1995 +0200
@@ -14,7 +14,7 @@
 val transrec2_0 = result();
 
 goal thy "(THE j. succ(i)=succ(j)) = i";
-by (fast_tac (AC_cs addSIs [the_equality]) 1);
+by (fast_tac (OrdQuant_cs addSIs [the_equality]) 1);
 val THE_succ_eq = result();
 
 goal thy "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))";
@@ -26,8 +26,8 @@
 goal thy "!!i. Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))";
 by (rtac (transrec2_def RS def_transrec RS trans) 1);
 by (resolve_tac [if_not_P RS trans] 1 THEN
-    fast_tac (AC_cs addSDs [Limit_has_0] addSEs [ltE]) 1);
+    fast_tac (OrdQuant_cs addSDs [Limit_has_0] addSEs [ltE]) 1);
 by (resolve_tac [if_not_P RS trans] 1 THEN
-    fast_tac (AC_cs addSEs [succ_LimitE]) 1);
-by (simp_tac AC_ss 1);
+    fast_tac (OrdQuant_cs addSEs [succ_LimitE]) 1);
+by (simp_tac OrdQuant_ss 1);
 val transrec2_Limit = result();