author | wenzelm |
Fri, 09 Aug 2013 00:04:47 +0200 | |
changeset 52928 | facb4f6dc391 |
parent 52927 | 9c6aef15a7ad |
child 52929 | 52d21bddcb8a |
--- 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;