Fixed a use of an outdated Substring function
authorpaulson
Thu, 22 Dec 2005 12:27:10 +0100
changeset 18489 151e52a4db3f
parent 18488 a353a61c4544
child 18490 434e34392c40
Fixed a use of an outdated Substring function
src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Dec 22 00:41:26 2005 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Thu Dec 22 12:27:10 2005 +0100
@@ -1216,7 +1216,7 @@
 
 fun split_name str =
     let
-	val sub = Substring.all str
+	val sub = Substring.full str
 	val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub)
 	val (newstr,u) = apboth Substring.string (Substring.splitr (fn c => c = #"_") f)
     in