# 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