Replaced obsolete "makestring" by Int.toString
authorpaulson
Wed, 27 Nov 1996 10:41:42 +0100
changeset 2239 8f9007a2f165
parent 2238 c72a23bbe762
child 2240 a8c074224e11
Replaced obsolete "makestring" by Int.toString
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;