src/HOL/Tools/res_atp.ML
changeset 16741 7a6c17b826c0
parent 16675 96bdc59afc05
child 16767 2d4433759b8d
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 07 18:24:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 07 18:25:02 2005 +0200
     1.3 @@ -287,10 +287,13 @@
     1.4  (******************************************************************)
     1.5  (*FIX changed to clasimp_file *)
     1.6  fun isar_atp' (ctxt,thms, thm) =
     1.7 + if null (prems_of thm) then () 
     1.8 + else
     1.9      let 
    1.10 -	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.11 +	val _= (print_mode := (Library.gen_rems (op =) 
    1.12 +	                       (! print_mode, ["xsymbols", "symbols"])))
    1.13          val _= (warning ("in isar_atp'"))
    1.14 -        val prems  = prems_of thm
    1.15 +        val prems = prems_of thm
    1.16          val sign = sign_of_thm thm
    1.17          val thms_string = Meson.concat_with_and (map string_of_thm thms) 
    1.18          val thmstring = string_of_thm thm
    1.19 @@ -298,22 +301,21 @@
    1.20          
    1.21  	(* set up variables for writing out the clasimps to a tptp file *)
    1.22  	val (clause_arr, num_of_clauses) =
    1.23 -	    ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
    1.24 +	    ResClasimp.write_out_clasimp (File.platform_path clasimp_file) 
    1.25  	                                 (ProofContext.theory_of ctxt)
    1.26 -        val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) )  
    1.27 -           
    1.28 -        
    1.29 +	                                 (hd prems) (*FIXME: hack!! need to do all prems*)
    1.30 +        val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) 
    1.31          val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
    1.32 -        val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    1.33 +        val pidstring = string_of_int(Word.toInt
    1.34 +                           (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    1.35      in
    1.36 -	case prems of [] => () 
    1.37 -		    | _ => ((warning ("initial thms: "^thms_string)); 
    1.38 -                           (warning ("initial thm: "^thmstring));
    1.39 -                           (warning ("subgoals: "^prems_string));
    1.40 -                           (warning ("pid: "^ pidstring))); 
    1.41 -                            isar_atp_aux thms thm (length prems) (childin, childout, pid) ;
    1.42 -                           (warning("turning xsymbol back on!"));
    1.43 -                           print_mode := (["xsymbols", "symbols"] @ ! print_mode)
    1.44 +       warning ("initial thms: "^thms_string); 
    1.45 +       warning ("initial thm: "^thmstring);
    1.46 +       warning ("subgoals: "^prems_string);
    1.47 +       warning ("pid: "^ pidstring); 
    1.48 +       isar_atp_aux thms thm (length prems) (childin, childout, pid);
    1.49 +       warning("turning xsymbol back on!");
    1.50 +       print_mode := (["xsymbols", "symbols"] @ ! print_mode)
    1.51      end;
    1.52  
    1.53