make SML/NJ happy
authorblanchet
Wed Aug 31 13:22:50 2011 +0200 (2011-08-31)
changeset 44626a40b713232c8
parent 44625 4a1132815a70
child 44627 134c06282ae6
make SML/NJ happy
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:52:03 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 13:22:50 2011 +0200
     1.3 @@ -1771,7 +1771,7 @@
     1.4  
     1.5  fun formula_line_for_free_type j phi =
     1.6    Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
     1.7 -fun formula_lines_for_free_types type_enc facts =
     1.8 +fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
     1.9    let
    1.10      val phis =
    1.11        fold (union (op =)) (map #atomic_types facts) []