# HG changeset patch
# User blanchet
# Date 1306852716 -7200
# Node ID bb0ceef7d39fad12f9b6f864c9bbef19b4916c98
# Parent  81d1b15aa0aed3ddb4826a3a55feca0ee0248395
no need for type arguments with "xxx_tags_heavy" type system

diff -r 81d1b15aa0ae -r bb0ceef7d39f src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue May 31 16:38:36 2011 +0200
@@ -616,18 +616,21 @@
     level_of_type_sys type_sys = All_Types andalso
     heaviness_of_type_sys type_sys = Heavy
 
-fun general_type_arg_policy type_sys =
-  if level_of_type_sys type_sys = No_Types then
-    No_Type_Args
-  else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
-    Mangled_Type_Args (should_drop_arg_type_args type_sys)
-  else
-    Explicit_Type_Args (should_drop_arg_type_args type_sys)
+fun general_type_arg_policy (Tags (_, All_Types, Heavy)) = No_Type_Args
+  | general_type_arg_policy type_sys =
+    if level_of_type_sys type_sys = No_Types then
+      No_Type_Args
+    else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
+      Mangled_Type_Args (should_drop_arg_type_args type_sys)
+    else
+      Explicit_Type_Args (should_drop_arg_type_args type_sys)
 
 fun type_arg_policy type_sys s =
   if s = @{const_name HOL.eq} orelse
      (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
     No_Type_Args
+  else if s = type_tag_name then
+    Explicit_Type_Args false
   else
     general_type_arg_policy type_sys