changeset 48081 | 6435b2c73038 |
parent 48080 | 512327d842c3 |
child 48087 | 94835838ed2c |
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jun 06 10:35:05 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jun 06 10:35:05 2012 +0200 @@ -860,7 +860,7 @@ else if poly = Mangled_Monomorphic then Mangled_Type_Args else if member (op =) monom_constrs s andalso - granularity_of_type_level level = Positively_Naked_Vars then + granularity_of_type_level level <> Ghost_Type_Arg_Vars then No_Type_Args else Explicit_Type_Args