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