remove needless typing information
authorblanchet
Mon Aug 22 15:02:45 2011 +0200 (2011-08-22)
changeset 44398d21f7e330ec8
parent 44397 06375952f1fa
child 44399 cd1e32b8d4c4
remove needless typing information
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -702,17 +702,17 @@
     1.4    else case type_enc of
     1.5      Tags (_, All_Types, Heavyweight) => No_Type_Args
     1.6    | _ =>
     1.7 -    if level_of_type_enc type_enc = No_Types orelse
     1.8 -       s = @{const_name HOL.eq} orelse
     1.9 -       (s = app_op_name andalso
    1.10 -        level_of_type_enc type_enc = Const_Arg_Types) then
    1.11 -      No_Type_Args
    1.12 -    else
    1.13 -      should_drop_arg_type_args type_enc
    1.14 -      |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.15 -            Mangled_Type_Args
    1.16 -          else
    1.17 -            Explicit_Type_Args)
    1.18 +    let val level = level_of_type_enc type_enc in
    1.19 +      if level = No_Types orelse s = @{const_name HOL.eq} orelse
    1.20 +         (s = app_op_name andalso level = Const_Arg_Types) then
    1.21 +        No_Type_Args
    1.22 +      else
    1.23 +        should_drop_arg_type_args type_enc
    1.24 +        |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.25 +              Mangled_Type_Args
    1.26 +            else
    1.27 +              Explicit_Type_Args)
    1.28 +    end
    1.29  
    1.30  (* Make literals for sorted type variables. *)
    1.31  fun generic_add_sorts_on_type (_, []) = I
    1.32 @@ -1919,7 +1919,8 @@
    1.33      val bounds = bound_names |> map (fn name => ATerm (name, []))
    1.34      val cst = mk_aterm format type_enc (s, s') T_args
    1.35      val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
    1.36 -    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
    1.37 +    val should_encode =
    1.38 +      should_encode_type ctxt nonmono_Ts (level_of_type_enc type_enc)
    1.39      val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE
    1.40      val add_formula_for_res =
    1.41        if should_encode res_T then
    1.42 @@ -1953,7 +1954,7 @@
    1.43    case type_enc of
    1.44      Simple_Types _ =>
    1.45      decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
    1.46 -  | Guards _ =>
    1.47 +  | Guards (_, level, _) =>
    1.48      let
    1.49        val decls =
    1.50          case decls of
    1.51 @@ -1968,8 +1969,7 @@
    1.52          | _ => decls
    1.53        val n = length decls
    1.54        val decls =
    1.55 -        decls |> filter (should_encode_type ctxt nonmono_Ts
    1.56 -                             (level_of_type_enc type_enc)
    1.57 +        decls |> filter (should_encode_type ctxt nonmono_Ts level
    1.58                           o result_type_of_decl)
    1.59      in
    1.60        (0 upto length decls - 1, decls)