1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jun 26 11:14:40 2012 +0200
     1.3 @@ -492,11 +492,14 @@
     1.4  fun string_of_arity (0, n) = string_of_int n
     1.5    | string_of_arity (m, n) = string_of_int m ^ "+" ^ string_of_int n
     1.6  
     1.7 +val dfg_class_inter = space_implode " & "
     1.8 +
     1.9  fun dfg_string_for_formula poly gen_simp info =
    1.10    let
    1.11      val str_for_typ = string_for_type (DFG poly)
    1.12      fun str_for_bound_typ (ty, []) = str_for_typ ty
    1.13 -      | str_for_bound_typ (ty, cls) = str_for_typ ty ^ " : " ^ commas cls
    1.14 +      | str_for_bound_typ (ty, cls) =
    1.15 +        str_for_typ ty ^ " : " ^ dfg_class_inter cls
    1.16      fun suffix_tag top_level s =
    1.17        if top_level then
    1.18          case extract_isabelle_status info of
    1.19 @@ -554,7 +557,7 @@
    1.20            |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
    1.21        in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
    1.22      fun str_for_bound_tvar (ty, []) = ty
    1.23 -      | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ commas cls
    1.24 +      | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ dfg_class_inter cls
    1.25      fun sort_decl xs ty cl =
    1.26        "sort(" ^
    1.27        (if null xs then ""