1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
     1.3 @@ -652,25 +652,31 @@
     1.4                          level)
     1.5                else
     1.6                  raise Same.SAME
     1.7 -            | (Raw_Monomorphic, _) => raise Same.SAME
     1.8 -            | (poly, All_Types) =>
     1.9 -              Native (Higher_Order THF_With_Choice, poly, All_Types))
    1.10 +            | (poly as Raw_Polymorphic _, All_Types) =>
    1.11 +              Native (Higher_Order THF_With_Choice, poly, All_Types)
    1.12 +            | _ => raise Same.SAME)
    1.13           | ("guards", (SOME poly, _)) =>
    1.14 -           if poly = Mangled_Monomorphic andalso
    1.15 -              granularity_of_type_level level = Undercover_Vars then
    1.16 +           if (poly = Mangled_Monomorphic andalso
    1.17 +               granularity_of_type_level level = Undercover_Vars) orelse
    1.18 +              poly = Type_Class_Polymorphic then
    1.19               raise Same.SAME
    1.20             else
    1.21               Guards (poly, level)
    1.22           | ("tags", (SOME poly, _)) =>
    1.23 -           if granularity_of_type_level level = Undercover_Vars then
    1.24 +           if granularity_of_type_level level = Undercover_Vars orelse
    1.25 +              poly = Type_Class_Polymorphic then
    1.26               raise Same.SAME
    1.27             else
    1.28               Tags (poly, level)
    1.29           | ("args", (SOME poly, All_Types (* naja *))) =>
    1.30 -           Guards (poly, Const_Types false)
    1.31 +           if poly = Type_Class_Polymorphic then raise Same.SAME
    1.32 +           else Guards (poly, Const_Types false)
    1.33           | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) =>
    1.34 -           if poly = Mangled_Monomorphic then raise Same.SAME
    1.35 -           else Guards (poly, Const_Types true)
    1.36 +           if poly = Mangled_Monomorphic orelse
    1.37 +              poly = Type_Class_Polymorphic then
    1.38 +             raise Same.SAME
    1.39 +           else
    1.40 +             Guards (poly, Const_Types true)
    1.41           | ("erased", (NONE, All_Types (* naja *))) =>
    1.42             Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types)
    1.43           | _ => raise Same.SAME)
    1.44 @@ -680,9 +686,13 @@
    1.45      Higher_Order THF_Without_Choice
    1.46    | adjust_order _ type_enc = type_enc
    1.47  
    1.48 +fun no_type_classes Type_Class_Polymorphic =
    1.49 +    Raw_Polymorphic With_Phantom_Type_Vars
    1.50 +  | no_type_classes poly = poly
    1.51 +
    1.52  fun adjust_type_enc (THF (Polymorphic, _, choice, _))
    1.53                      (Native (order, poly, level)) =
    1.54 -    Native (adjust_order choice order, poly, level)
    1.55 +    Native (adjust_order choice order, no_type_classes poly, level)
    1.56    | adjust_type_enc (THF (Monomorphic, _, choice, _))
    1.57                           (Native (order, _, level)) =
    1.58      Native (adjust_order choice order, Mangled_Monomorphic, level)
    1.59 @@ -693,9 +703,9 @@
    1.60    | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) =
    1.61      Native (First_Order, Mangled_Monomorphic, level)
    1.62    | adjust_type_enc (TFF _) (Native (_, poly, level)) =
    1.63 -    Native (First_Order, poly, level)
    1.64 +    Native (First_Order, no_type_classes poly, level)
    1.65    | adjust_type_enc format (Native (_, poly, level)) =
    1.66 -    adjust_type_enc format (Guards (poly, level))
    1.67 +    adjust_type_enc format (Guards (no_type_classes poly, level))
    1.68    | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
    1.69      (if is_type_enc_sound type_enc then Tags else Guards) stuff
    1.70    | adjust_type_enc _ type_enc = type_enc