# HG changeset patch
# User paulson
# Date 849087702 -3600
# Node ID 8f9007a2f1658c5d51a2bb98809e0ae3186686b2
# Parent  c72a23bbe76218115e2cfc166f2b22f3db1fc15e
Replaced obsolete "makestring" by Int.toString

diff -r c72a23bbe762 -r 8f9007a2f165 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Wed Nov 27 10:40:45 1996 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Wed Nov 27 10:41:42 1996 +0100
@@ -64,7 +64,7 @@
 
 fun name_in_term (name,Const (s,t))     =(name=s)
   | name_in_term (name,Free (s,t))      =(name=s)
-  | name_in_term (name,Var ((s,i),t))   =(name=s ^ makestring i)
+  | name_in_term (name,Var ((s,i),t))   =(name=s ^ Int.toString i)
   | name_in_term (name,Abs (s,t,trm))   =(name=s) orelse (name_in_term (name,trm))
   | name_in_term (name,trm1 $ trm2)     =(name_in_term (name,trm1)) orelse (name_in_term (name,trm2))
   | name_in_term (_,_)                  =false;