src/HOL/Tools/ATP/recon_prelim.ML

 open Utils;
 open Envir;
 open Tfl;
 open Rules;
 
-goal Main.thy "A -->A";
+Goal "A -->A";
 by Auto_tac;
 qed "foo";
 
 
 val Mainsign = #sign (rep_thm foo);