| changeset 18489 | 151e52a4db3f |
| parent 18358 | 0a733e11021a |
| child 18678 | dd0c569fa43d |
--- 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