# HG changeset patch
# User paulson
# Date 993476215 -7200
# Node ID 5c84a5ca3a21473166e59937488e44e65a42ba3d
# Parent  0f16ad464c62b8b9cb7a6b6934d8809b1c5fab68
Simprocs for type "nat" no longer introduce numerals unless

diff -r 0f16ad464c62 -r 5c84a5ca3a21 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Jun 25 15:35:59 2001 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Mon Jun 25 15:36:55 2001 +0200
@@ -110,7 +110,7 @@
 Goal "f:BufEq ==> ? l. !i x s. s:BufAC_Asm --> x << s --> Fin (l i) < #x --> \
 		\    (x,f\\<cdot>x):down_iterate BufAC_Cmt_F i --> \
 		\    (s,f\\<cdot>s):down_iterate BufAC_Cmt_F i";
-by (res_inst_tac [("x","%i. i+i")] exI 1);
+by (res_inst_tac [("x","%i. #2*i")] exI 1);
 by (rtac allI 1);
 by (nat_ind_tac "i" 1);
 by ( Simp_tac 1);