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_wrapper.ML
changeset 31410 c231efe693ce
parent 31409 d8537ba165b5
child 31411 1d00ab68bc8d 
--- a/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -68,13 +68,13 @@
       case axiom_clauses of
           NONE => relevance_filter goal goal_cls
         | SOME axcls => axcls
-    val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy
+    val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
     val the_const_counts = case const_counts of
       NONE =>
         ResHolClause.count_constants(
           case axiom_clauses of
             NONE => clauses
-            | SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy)
+            | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
           )
       | SOME ccs => ccs
     val _ = writer fname the_const_counts clauses
isabelle