# HG changeset patch
# User wenzelm
# Date 1375999487 -7200
# Node ID facb4f6dc39173824935f37445acf7d071be5046
# Parent  9c6aef15a7ad3aadf4498361bdcf4fc0be38c9be
more explicit error;

diff -r 9c6aef15a7ad -r facb4f6dc391 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 00:02:18 2013 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 00:04:47 2013 +0200
@@ -574,6 +574,8 @@
 
 val _ =
   Query_Operation.register "find_theorems" (fn st => fn args =>
-    Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args)));
+    if can Toplevel.theory_of st then
+      Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
+    else error "Unknown theory context");
 
 end;