# HG changeset patch
# User desharna
# Date 1740739019 -3600
# Node ID b3502f81ab3d7071918668e60d4647d7c54fab2a
# Parent  4a21e6973e1133a456cf5bc9c9c93166f39e1891
tuned signature

diff -r 4a21e6973e11 -r b3502f81ab3d 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