src/HOL/Tools/res_atp.ML
changeset 16061 8a139c1557bf
parent 16039 dfe264950511
child 16089 9169bdf930f8
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 24 07:43:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 24 10:23:24 2005 +0200
     1.3 @@ -245,19 +245,18 @@
     1.4  (**********************************************)
     1.5  
     1.6  fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
     1.7 -                  	if (k > n) 
     1.8 -                        then () 
     1.9 -	  		else 
    1.10 -                           (let val  prems = prems_of thm 
    1.11 -                                val sg_term = get_nth n prems
    1.12 -                                val thmstring = string_of_thm thm
    1.13 -                            in   
    1.14 -                                 
    1.15 -                		(warning("in isar_atp_goal'"));
    1.16 -                                (warning("thmstring in isar_atp_goal': "^thmstring));
    1.17 - 				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
    1.18 -                                 isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
    1.19 -                            end);
    1.20 +      if (k > n) 
    1.21 +      then () 
    1.22 +      else 
    1.23 +	  let val  prems = prems_of thm 
    1.24 +	      val sg_term = ReconOrderClauses.get_nth n prems
    1.25 +	      val thmstring = string_of_thm thm
    1.26 +	  in   
    1.27 +	      (warning("in isar_atp_goal'"));
    1.28 +	      (warning("thmstring in isar_atp_goal': "^thmstring));
    1.29 +	       isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
    1.30 +	       isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
    1.31 +	  end;
    1.32  
    1.33  
    1.34  fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) =