Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 20293 e7bed14f4de2
parent 20247 32fb8d2715de 
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Aug 02 22:26:46 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Aug 02 22:26:47 2006 +0200
@@ -205,7 +205,7 @@
 
      val clauses = make_clauses thms    (*FIXME: must this be repeated??*)
      
-     val vars = map thm_vars clauses
+     val vars = map thm_varnames clauses
     
      val distvars = distinct (op =) (fold append vars [])
      val clause_terms = map prop_of clauses  
@@ -228,12 +228,12 @@
      (* get list of axioms as thms with their variables *)
 
      val ax_metas = get_assoc_snds ax_strs metas_and_strs []
-     val ax_vars = map thm_vars ax_metas
+     val ax_vars = map thm_varnames ax_metas
      val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
 
      (* get list of extra axioms as thms with their variables *)
      val extra_metas = add_if_not_inlist Thm.eq_thm metas ax_metas []
-     val extra_vars = map thm_vars extra_metas
+     val extra_vars = map thm_varnames extra_metas
      val extra_with_vars = if not (null extra_metas)
 			   then ListPair.zip (extra_metas,extra_vars)
 			   else []
isabelle