# HG changeset patch
# User wenzelm
# Date 1695560860 -7200
# Node ID ff7db9055002b7735b937820aaa85d0b39992f4a
# Parent  5fe4c11b5ecbeb957d084cee1424535f918eb58a
clarified signature;

diff -r 5fe4c11b5ecb -r ff7db9055002 src/Pure/Concurrent/isabelle_thread.ML
--- a/src/Pure/Concurrent/isabelle_thread.ML	Sun Sep 24 11:42:13 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML	Sun Sep 24 15:07:40 2023 +0200
@@ -24,6 +24,8 @@
   val interrupt_exn: 'a Exn.result
   val interrupt_self: unit -> 'a
   val interrupt_other: T -> unit
+  val try: (unit -> 'a) -> 'a option
+  val can: (unit -> 'a) -> bool
 end;
 
 structure Isabelle_Thread: ISABELLE_THREAD =
@@ -115,4 +117,7 @@
 fun interrupt_other t =
   Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
 
+fun try e = Basics.try e ();
+fun can e = Basics.can e ();
+
 end;
diff -r 5fe4c11b5ecb -r ff7db9055002 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 11:42:13 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:07:40 2023 +0200
@@ -343,8 +343,8 @@
 (* special forms for option type *)
 
 val _ = Theory.setup
- (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #>
-  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can" #>
+ (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "Isabelle_Thread.try" #>
+  ML_Antiquotation.special_form \<^binding>\<open>can\<close> "Isabelle_Thread.can" #>
   ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
     (fn _ => fn src => fn ctxt =>
       let