src/HOL/Tools/res_atp.ML
changeset 22578 b0eb5652f210
parent 22422 ee19cdb07528
child 22645 8a70bc644833
--- a/src/HOL/Tools/res_atp.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -900,7 +900,7 @@
       last_watcher_pid := SOME (childin, childout, pid, files);
       Output.debug (fn () => "problem files: " ^ space_implode ", " files);
       Output.debug (fn () => "pid: " ^ string_of_pid pid);
-      watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
+      watcher_call_provers (Thm.theory_of_thm th) (Thm.prems_of th) (childin, childout, pid)
     end;
 
 (*For ML scripts, and primarily, for debugging*)