stricted type encoding parsing
authorblanchet
Wed Sep 07 21:31:21 2011 +0200 (2011-09-07)
changeset 44810c1c05a578c1a
parent 44800 0472f2367efb
child 44811 0bff1a4228b3
stricted type encoding parsing
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 20:29:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 21:31:21 2011 +0200
     1.3 @@ -591,6 +591,9 @@
     1.4         | NONE => (constr Heavy, s))
     1.5    | NONE => fallback s
     1.6  
     1.7 +fun is_mangled_arg_light poly level =
     1.8 +  poly = Mangled_Monomorphic andalso heaviness_of_level level = Arg_Light
     1.9 +
    1.10  fun type_enc_from_string soundness s =
    1.11    (case try (unprefix "poly_") s of
    1.12       SOME s => (SOME Polymorphic, s)
    1.13 @@ -627,9 +630,12 @@
    1.14                else
    1.15                  raise Same.SAME
    1.16              | _ => raise Same.SAME)
    1.17 -         | ("guards", (SOME poly, _)) => Guards (poly, level)
    1.18 -         | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
    1.19 -         | ("tags", (SOME poly, _)) => Tags (poly, level)
    1.20 +         | ("guards", (SOME poly, _)) =>
    1.21 +           if is_mangled_arg_light poly level then raise Same.SAME
    1.22 +           else Guards (poly, level)
    1.23 +         | ("tags", (SOME poly, _)) =>
    1.24 +           if is_mangled_arg_light poly level then raise Same.SAME
    1.25 +           else Tags (poly, level)
    1.26           | ("args", (SOME poly, All_Types (* naja *))) =>
    1.27             Guards (poly, Const_Arg_Types)
    1.28           | ("erased", (NONE, All_Types (* naja *))) =>