# HG changeset patch
# User berghofe
# Date 835357869 -7200
# Node ID e1458e1a9f80290fc66ac42b431ffaa3a1cb7115
# Parent  c192d7dc22e78b0d965b8d5b1fa5c21cfdd8f4e4
Replaced occurrence of fast_tac by Fast_tac .

diff -r c192d7dc22e7 -r e1458e1a9f80 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Jun 21 13:39:08 1996 +0200
+++ b/src/HOL/Nat.ML	Fri Jun 21 13:51:09 1996 +0200
@@ -462,7 +462,7 @@
         "!!m. Suc m <= n ==> m < n";
 by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
 by (cut_facts_tac [less_linear] 1);
-by (fast_tac HOL_cs 1);
+by (Fast_tac 1);
 qed "Suc_le_lessD";
 
 goal Nat.thy "(Suc m <= n) = (m < n)";