src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Fri Feb 28 11:13:13 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Fri Feb 28 11:36:59 2025 +0100
@@ -6,7 +6,6 @@
 
 signature TRY0 =
 sig
-  val noneN : string
   val silence_methods : bool -> Proof.context -> Proof.context
   datatype modifier = Use | Simp | Intro | Elim | Dest
   type xthm = Facts.ref * Token.src list