diff -r 5dbe1a269999 -r 0677712016b5 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Oct 24 16:45:09 2024 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Oct 24 16:46:25 2024 +0200
@@ -8,7 +8,7 @@
 sig
   val noneN : string
   val silence_methods : bool -> Proof.context -> Proof.context
-  datatype modifier = Simp | Intro | Elim | Dest
+  datatype modifier = Use | Simp | Intro | Elim | Dest
   type result = {name: string, command: string, time: int, state: Proof.state}
   val try0 : Time.time option -> ((Facts.ref * Token.src list)  * modifier list) list -> 
     Proof.state -> result list
@@ -44,7 +44,7 @@
   |> Scan.read Token.stopper Method.parse
   |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
 
-datatype modifier = Simp | Intro | Elim | Dest
+datatype modifier = Use | Simp | Intro | Elim | Dest
 
 fun string_of_xthm (xref, args) =
   Facts.string_of_ref xref ^