more explicit error;
authorwenzelm
Fri Aug 09 00:04:47 2013 +0200 (2013-08-09)
changeset 52928facb4f6dc391
parent 52927 9c6aef15a7ad
child 52929 52d21bddcb8a
more explicit error;
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 09 00:02:18 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 09 00:04:47 2013 +0200
     1.3 @@ -574,6 +574,8 @@
     1.4  
     1.5  val _ =
     1.6    Query_Operation.register "find_theorems" (fn st => fn args =>
     1.7 -    Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args)));
     1.8 +    if can Toplevel.theory_of st then
     1.9 +      Pretty.string_of (pretty_theorems_cmd st NONE false (maps (read_query Position.none) args))
    1.10 +    else error "Unknown theory context");
    1.11  
    1.12  end;