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.
tuned --- more robust ML patterns;
authorwenzelm
Thu, 29 Dec 2022 12:08:58 +0100
changeset 76810 3f211d126ddc
parent 76809 f05327293f07
child 76811 56d76e8cecf4
tuned --- more robust ML patterns;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/toplevel.ML	Thu Dec 29 11:49:11 2022 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Dec 29 12:08:58 2022 +0100
@@ -328,7 +328,7 @@
   | apply_union int (tr :: trs) state =
       apply_union int trs state
         handle Runtime.UNDEF => apply_tr int tr state
-          | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state
+          | FAILURE (alt_state, Runtime.UNDEF) => apply_tr int tr alt_state
           | exn as FAILURE _ => raise exn
           | exn => raise FAILURE (state, exn);
 
@@ -644,7 +644,7 @@
 fun app int (tr as Transition {name, markers, trans, ...}) =
   setmp_thread_position tr
     (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans)
-      ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)
+      ##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn)
       #> show_state);
 
 in
isabelle