src/Pure/Tools/find_theorems.ML
changeset 52928 facb4f6dc391
parent 52927 9c6aef15a7ad
child 52940 6fce81e92e7c
--- 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;