Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more direct clone (see also change of exception in 8d8c70b41bab);
authorwenzelm
Fri, 14 Apr 2023 21:39:10 +0200
changeset 77848 d73451fb7162
parent 77847 3bb6468d202e
child 77849 ba563d3f73ff
more direct clone (see also change of exception in 8d8c70b41bab);
src/Pure/library.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle