src/HOL/Import/proof_kernel.ML

 	fn th => eq_set(t_consts,add_consts(prop_of th,[]))
     end
 
 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
 	if not (idx = "") andalso u = "_"
 	then SOME (newstr,valOf(Int.fromString idx))