# HG changeset patch
# User paulson
# Date 1135250830 -3600
# Node ID 151e52a4db3fd5363f5b0c8bdba046658b09b734
# Parent  a353a61c4544939f4c31a076036d3688ee5555bd
Fixed a use of an outdated Substring function

diff -r a353a61c4544 -r 151e52a4db3f 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