src/HOL/Tools/try0.ML
changeset 82397 ae2af2e085fd
parent 82396 7230281bde03
child 82455 eaf0b4673ab2
--- a/src/HOL/Tools/try0.ML	Wed Apr 02 11:18:35 2025 +0200
+++ b/src/HOL/Tools/try0.ML	Fri Apr 04 15:27:28 2025 +0200
@@ -107,7 +107,7 @@
 
 fun get_proof_method_or_noop name =
   (case get_proof_method name of
-    NONE => noop_proof_method
+    NONE => (warning ("Proof method \"" ^ name ^ "\" is undefined"); noop_proof_method)
   | SOME proof_method => proof_method)
 
 fun maybe_apply_proof_method name mode : proof_method =