Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
make SML/NJ happy
authorblanchet
Wed, 31 Aug 2011 13:22:50 +0200
changeset 44626 a40b713232c8
parent 44625 4a1132815a70
child 44627 134c06282ae6
make SML/NJ happy
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:52:03 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 13:22:50 2011 +0200
@@ -1771,7 +1771,7 @@
 
 fun formula_line_for_free_type j phi =
   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
-fun formula_lines_for_free_types type_enc facts =
+fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
   let
     val phis =
       fold (union (op =)) (map #atomic_types facts) []
isabelle