src/HOL/Tools/ATP/recon_translate_proof.ML

 *)
 
 structure ReconTranslateProof =
 struct
 
-fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
+fun thm_varnames thm =
+  (Drule.fold_terms o Term.fold_aterms)
+    (fn Var ((x, _), _) => insert (op =) x | _ => I) thm [];
 
 exception Reflex_equal;
 
 (********************************)
 (* Proofstep datatype           *)

 (************************************************)
 
 fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
     let val this_axiom = (the o AList.lookup (op =) clauses) clausenum
 	val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)         
-	val thmvars = thm_vars res
+	val thmvars = thm_varnames res
     in
 	(res, (Axiom,clause_strs,thmvars )  )
     end
     handle Option => reconstruction_failed "follow_axiom"
 

 fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
     let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
 	val thm2 =  (the o AList.lookup (op =) thml) clause2
 	val res =   thm1 RSN ((lit2 +1), thm2)
 	val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
-	val thmvars = thm_vars res
+	val thmvars = thm_varnames res
     in
        (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
     end
     handle Option => reconstruction_failed "follow_binary"
 

     let val thm1 =  select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1)
 	val thm2 =  (the o AList.lookup (op =) thml) clause2
 	val res =   thm1 RSN ((lit2 +1), thm2)
 	val (res', numlist, symlist, nsymlist) = 
 	    (ReconOrderClauses.rearrange_clause res clause_strs allvars)
-	val thmvars = thm_vars res
+	val thmvars = thm_varnames res
     in
        (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
     end
     handle Option => reconstruction_failed "follow_mrr"
 

 	     val str2 = lit_string_with_nums t2;
 	     val facthm = read_instantiate [(str1,str2)] th;
 	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
 	     val (res', numlist, symlist, nsymlist) = 
 	         ReconOrderClauses.rearrange_clause res clause_strs allvars
-	     val thmvars = thm_vars res'
+	     val thmvars = thm_varnames res'
 	  in 
 		 (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
 	  end
       else
 	  let

 	     val str1 = lit_string_with_nums t2;
 	     val facthm = read_instantiate [(str1,str2)] th;
 	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
 	     val (res', numlist, symlist, nsymlist) = 
 	         ReconOrderClauses.rearrange_clause res clause_strs allvars
-	     val thmvars = thm_vars res'
+	     val thmvars = thm_varnames res'
 	  in 
 		 (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
 	  end
    end
    handle Option => reconstruction_failed "follow_factor"

 		   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
 		   val newth' =negate_head newth 
 		in 
 		   ReconOrderClauses.rearrange_clause newth' clause_strs allvars
 		end)
-      val thmvars = thm_vars res
+      val thmvars = thm_varnames res
    in 
      (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
    end
    handle Option => reconstruction_failed "follow_standard_para"
 

 	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
      	  val newthm = negate_head newth
 	  val newthm' = delete_assumps eq_lit_prem_num newthm
 	  val (res, numlist, symlist, nsymlist) =
 	      ReconOrderClauses.rearrange_clause newthm clause_strs allvars
-	  val thmvars = thm_vars res
+	  val thmvars = thm_varnames res
        in
 	   (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
        end
        handle Option => reconstruction_failed "follow_rewrite"
 

 	val prems1 = prems_of th1
 	val newthm = refl RSN ((lit1+ 1), th1)
 		     handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
 	val (res, numlist, symlist, nsymlist) =
 	    ReconOrderClauses.rearrange_clause newthm clause_strs allvars
-	val thmvars = thm_vars res
+	val thmvars = thm_varnames res
     in 
 	(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
     end
     handle Option => reconstruction_failed "follow_obvious"