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