# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID d21f7e330ec8673eb9ebabf18b9b9eb593d08f66
# Parent  06375952f1fab4e45ba0ce5f8e7d45caa75b9b52
remove needless typing information

diff -r 06375952f1fa -r d21f7e330ec8 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -702,17 +702,17 @@
   else case type_enc of
     Tags (_, All_Types, Heavyweight) => No_Type_Args
   | _ =>
-    if level_of_type_enc type_enc = No_Types orelse
-       s = @{const_name HOL.eq} orelse
-       (s = app_op_name andalso
-        level_of_type_enc type_enc = Const_Arg_Types) then
-      No_Type_Args
-    else
-      should_drop_arg_type_args type_enc
-      |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
-            Mangled_Type_Args
-          else
-            Explicit_Type_Args)
+    let val level = level_of_type_enc type_enc in
+      if level = No_Types orelse s = @{const_name HOL.eq} orelse
+         (s = app_op_name andalso level = Const_Arg_Types) then
+        No_Type_Args
+      else
+        should_drop_arg_type_args type_enc
+        |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
+              Mangled_Type_Args
+            else
+              Explicit_Type_Args)
+    end
 
 (* Make literals for sorted type variables. *)
 fun generic_add_sorts_on_type (_, []) = I
@@ -1919,7 +1919,8 @@
     val bounds = bound_names |> map (fn name => ATerm (name, []))
     val cst = mk_aterm format type_enc (s, s') T_args
     val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
-    val should_encode = should_encode_type ctxt nonmono_Ts All_Types
+    val should_encode =
+      should_encode_type ctxt nonmono_Ts (level_of_type_enc type_enc)
     val tag_with = tag_with_type ctxt format nonmono_Ts type_enc NONE
     val add_formula_for_res =
       if should_encode res_T then
@@ -1953,7 +1954,7 @@
   case type_enc of
     Simple_Types _ =>
     decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
-  | Guards _ =>
+  | Guards (_, level, _) =>
     let
       val decls =
         case decls of
@@ -1968,8 +1969,7 @@
         | _ => decls
       val n = length decls
       val decls =
-        decls |> filter (should_encode_type ctxt nonmono_Ts
-                             (level_of_type_enc type_enc)
+        decls |> filter (should_encode_type ctxt nonmono_Ts level
                          o result_type_of_decl)
     in
       (0 upto length decls - 1, decls)