src/HOL/Tools/ATP/watcher.ML

                                                               val clauses = make_clauses [thm]
                                                               val numcls =  zip  (numlist (length clauses)) (map make_meta_clause clauses)
                                                          
                                                           in
                                                              Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
-                                                             apply_res_thm reconstr goalstring;
+                                                             Recon_Transfer.apply_res_thm reconstr goalstring;
                                                              Pretty.writeln(Pretty.str  (oct_char "361"));
                                                              killWatcher childpid; () 
                                                           end
                                                        else
                                                            Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));

                                                   if ( (substring (reconstr, 0,1))= "[")
                                                   then 
 
                                                             (
                                                                  Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
-                                                                 apply_res_thm reconstr goalstring;
+                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
                                                                  Pretty.writeln(Pretty.str  (oct_char "361"));
                                                                  
                                                                  goals_being_watched := ((!goals_being_watched) - 1);
                                                          
                                                                  if ((!goals_being_watched) = 0)