# HG changeset patch
# User paulson
# Date 936798251 -7200
# Node ID 65f0cec65fc6a88141cd03e7e72cb238e0b2c911
# Parent  8e4a21d1ba4fc15b97a006064ae3177bd2f6c955
now uses the identity function

diff -r 8e4a21d1ba4f -r 65f0cec65fc6 src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Wed Sep 08 15:41:58 1999 +0200
+++ b/src/HOL/UNITY/Common.ML	Wed Sep 08 15:44:11 1999 +0200
@@ -73,7 +73,7 @@
 \               n: common |]  \
 \     ==> F : (atMost n) LeadsTo common";
 by (rtac LeadsTo_weaken_R 1);
-by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
+by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac subset_refl 2);
 by (blast_tac (claset() addDs [PSP_Stable2]