# HG changeset patch
# User wenzelm
# Date 1696784735 -7200
# Node ID 45ff003d337c802d9e90803b1a7db96b895d759f
# Parent  08fedb5bdeb0810ea2d718b9a105dbaf4d2132d3
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);

diff -r 08fedb5bdeb0 -r 45ff003d337c src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Oct 08 15:12:59 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun Oct 08 19:05:35 2023 +0200
@@ -27,7 +27,7 @@
   val interrupt_other: T -> unit
   structure Exn: EXN
   val expose_interrupt_result: unit -> unit Exn.result
-  val expose_interrupt: unit -> unit  (*exception Interrupt*)
+  val expose_interrupt: unit -> unit  (*exception Exn.is_interrupt*)
   val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a
   val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a
   val try: (unit -> 'a) -> 'a option
diff -r 08fedb5bdeb0 -r 45ff003d337c src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Sun Oct 08 15:12:59 2023 +0200
+++ b/src/Pure/ML/ml_init.ML	Sun Oct 08 19:05:35 2023 +0200
@@ -8,7 +8,7 @@
 
 val _ =
   List.app ML_Name_Space.forget_val
-    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
+    ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat", "Interrupt"];
 
 val ord = SML90.ord;
 val chr = SML90.chr;
@@ -19,8 +19,6 @@
 
 val error_depth = PolyML.error_depth;
 
-datatype illegal = Interrupt;
-
 structure Basic_Exn: BASIC_EXN = Exn;
 open Basic_Exn;
 
diff -r 08fedb5bdeb0 -r 45ff003d337c src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Oct 08 15:12:59 2023 +0200
+++ b/src/Pure/Pure.thy	Sun Oct 08 19:05:35 2023 +0200
@@ -1559,5 +1559,6 @@
 declare [[ML_write_global = false]]
 
 ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>
+ML_command \<open>\<^assert> (not (can ML_command \<open>() handle Interrupt => ()\<close>))\<close>
 
 end