# HG changeset patch
# User wenzelm
# Date 1672312138 -3600
# Node ID 3f211d126ddceecb4158bc5f637996e517c04ea4
# Parent  f05327293f07dc0886471c6c7328092ca0b1c5af
tuned --- more robust ML patterns;

diff -r f05327293f07 -r 3f211d126ddc src/Pure/Isar/toplevel.ML
--- 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