1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
     1.3 @@ -2184,19 +2184,24 @@
     1.4             |> bound_tvars type_enc true atomic_types, NONE, [])
     1.5  
     1.6  fun lines_for_free_types type_enc (facts : ifact list) =
     1.7 -  let
     1.8 -    fun line j (cl, T) =
     1.9 -      if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
    1.10 -        Class_Memb (class_memb_prefix ^ string_of_int j, [],
    1.11 -                    native_ho_type_from_typ type_enc false 0 T,
    1.12 -                    `make_class cl)
    1.13 -      else
    1.14 -        Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
    1.15 -                 class_atom type_enc (cl, T), NONE, [])
    1.16 -    val membs =
    1.17 -      fold (union (op =)) (map #atomic_types facts) []
    1.18 -      |> class_membs_for_types type_enc add_sorts_on_tfree
    1.19 -  in map2 line (0 upto length membs - 1) membs end
    1.20 +  if is_type_enc_polymorphic type_enc then
    1.21 +    let
    1.22 +      val type_classes =
    1.23 +        (polymorphism_of_type_enc type_enc = Type_Class_Polymorphic)
    1.24 +      fun line j (cl, T) =
    1.25 +        if type_classes then
    1.26 +          Class_Memb (class_memb_prefix ^ string_of_int j, [],
    1.27 +                      native_ho_type_from_typ type_enc false 0 T,
    1.28 +                      `make_class cl)
    1.29 +        else
    1.30 +          Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
    1.31 +                   class_atom type_enc (cl, T), NONE, [])
    1.32 +      val membs =
    1.33 +        fold (union (op =)) (map #atomic_types facts) []
    1.34 +        |> class_membs_for_types type_enc add_sorts_on_tfree
    1.35 +    in map2 line (0 upto length membs - 1) membs end
    1.36 +  else
    1.37 +    []
    1.38  
    1.39  (** Symbol declarations **)
    1.40