# HG changeset patch
# User blanchet
# Date 1315423881 -7200
# Node ID c1c05a578c1a7ae700c0a5399091ed2ea62d461e
# Parent  0472f2367efb86a15d6fab44288d4e0d26834bd7
stricted type encoding parsing

diff -r 0472f2367efb -r c1c05a578c1a src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 20:29:54 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
@@ -591,6 +591,9 @@
        | NONE => (constr Heavy, s))
   | NONE => fallback s
 
+fun is_mangled_arg_light poly level =
+  poly = Mangled_Monomorphic andalso heaviness_of_level level = Arg_Light
+
 fun type_enc_from_string soundness s =
   (case try (unprefix "poly_") s of
      SOME s => (SOME Polymorphic, s)
@@ -627,9 +630,12 @@
               else
                 raise Same.SAME
             | _ => raise Same.SAME)
-         | ("guards", (SOME poly, _)) => Guards (poly, level)
-         | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
-         | ("tags", (SOME poly, _)) => Tags (poly, level)
+         | ("guards", (SOME poly, _)) =>
+           if is_mangled_arg_light poly level then raise Same.SAME
+           else Guards (poly, level)
+         | ("tags", (SOME poly, _)) =>
+           if is_mangled_arg_light poly level then raise Same.SAME
+           else Tags (poly, level)
          | ("args", (SOME poly, All_Types (* naja *))) =>
            Guards (poly, Const_Arg_Types)
          | ("erased", (NONE, All_Types (* naja *))) =>