cleanup "simple" type encodings
authorblanchet
Tue Sep 06 11:31:01 2011 +0200 (2011-09-06)
changeset 4474268e34e7f01ab
parent 44741 600d26952759
child 44743 804dfa6d35b6
cleanup "simple" type encodings
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 17:50:04 2011 +0900
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 11:31:01 2011 +0200
     1.3 @@ -579,14 +579,18 @@
     1.4    |> (fn (poly, (level, (uniformity, core))) =>
     1.5           case (core, (poly, level, uniformity)) of
     1.6             ("simple", (SOME poly, _, Nonuniform)) =>
     1.7 -           (case poly of
     1.8 -              Raw_Monomorphic => raise Same.SAME
     1.9 -            | _ => Simple_Types (First_Order, poly, level))
    1.10 +           (case (poly, level) of
    1.11 +              (Polymorphic, All_Types) =>
    1.12 +              Simple_Types (First_Order, Polymorphic, All_Types)
    1.13 +            | (Mangled_Monomorphic, _) =>
    1.14 +              Simple_Types (First_Order, Mangled_Monomorphic, level)
    1.15 +            | _ => raise Same.SAME)
    1.16           | ("simple_higher", (SOME poly, _, Nonuniform)) =>
    1.17             (case (poly, level) of
    1.18 -              (Raw_Monomorphic, _) => raise Same.SAME
    1.19 -            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.20 -            | _ => Simple_Types (Higher_Order, poly, level))
    1.21 +              (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.22 +            | (Mangled_Monomorphic, _) =>
    1.23 +              Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    1.24 +            | _ => raise Same.SAME)
    1.25           | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    1.26           | ("tags", (SOME Polymorphic, _, _)) =>
    1.27             Tags (Polymorphic, level, uniformity)