src/HOL/Tools/ATP/atp_translate.ML
changeset 44418 800baa1b1406
parent 44416 cabd06b69c18
child 44450 d848dd7b21f4
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Aug 23 14:44:19 2011 +0200
     1.3 @@ -612,7 +612,7 @@
     1.4    | is_type_level_monotonicity_based _ = false
     1.5  
     1.6  fun adjust_type_enc (THF _) type_enc = type_enc
     1.7 -  | adjust_type_enc TFF (Simple_Types (Higher_Order, level)) =
     1.8 +  | adjust_type_enc TFF (Simple_Types (_, level)) =
     1.9      Simple_Types (First_Order, level)
    1.10    | adjust_type_enc format (Simple_Types (_, level)) =
    1.11      adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))