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/res_atp.ML
changeset 19617 7cb4b67d4b97
parent 19490 bf7f8347174a
child 19641 f1de44e61ec1 
--- a/src/HOL/Tools/res_atp.ML	Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu May 11 19:19:31 2006 +0200
@@ -269,9 +269,7 @@
 
 fun cnf_hyps_thms ctxt = 
     let val ths = ProofContext.prems_of ctxt
-    in
-	ResClause.union_all (map ResAxioms.skolem_thm ths)
-    end;
+    in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
 
 
 (**** write to files ****)
isabelle