# HG changeset patch
# User wenzelm
# Date 1681501150 -7200
# Node ID d73451fb71623e14bdbc6912cdf6423b09be2e2c
# Parent  3bb6468d202e8079e0ef088895ee0da5cc85c84f
more direct clone (see also change of exception in 8d8c70b41bab);

diff -r 3bb6468d202e -r d73451fb7162 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 14 21:34:51 2023 +0200
+++ b/src/Pure/library.ML	Fri Apr 14 21:39:10 2023 +0200
@@ -693,10 +693,7 @@
 
 (* functions tuned for strings, avoiding explode *)
 
-fun nth_string str i =
-  (case try String.substring (str, i, 1) of
-    SOME s => s
-  | NONE => raise Subscript);
+fun nth_string str i = String.substring (str, i, 1);
 
 fun fold_string f str x0 =
   let