# HG changeset patch
# User blanchet
# Date 1315301461 -7200
# Node ID 68e34e7f01ab734794a020653a9bd4579ce19037
# Parent  600d269527590964952effc6444213f0daed819a
cleanup "simple" type encodings

diff -r 600d26952759 -r 68e34e7f01ab src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 17:50:04 2011 +0900
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 11:31:01 2011 +0200
@@ -579,14 +579,18 @@
   |> (fn (poly, (level, (uniformity, core))) =>
          case (core, (poly, level, uniformity)) of
            ("simple", (SOME poly, _, Nonuniform)) =>
-           (case poly of
-              Raw_Monomorphic => raise Same.SAME
-            | _ => Simple_Types (First_Order, poly, level))
+           (case (poly, level) of
+              (Polymorphic, All_Types) =>
+              Simple_Types (First_Order, Polymorphic, All_Types)
+            | (Mangled_Monomorphic, _) =>
+              Simple_Types (First_Order, Mangled_Monomorphic, level)
+            | _ => raise Same.SAME)
          | ("simple_higher", (SOME poly, _, Nonuniform)) =>
            (case (poly, level) of
-              (Raw_Monomorphic, _) => raise Same.SAME
-            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
-            | _ => Simple_Types (Higher_Order, poly, level))
+              (_, Noninf_Nonmono_Types _) => raise Same.SAME
+            | (Mangled_Monomorphic, _) =>
+              Simple_Types (Higher_Order, Mangled_Monomorphic, level)
+            | _ => raise Same.SAME)
          | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
          | ("tags", (SOME Polymorphic, _, _)) =>
            Tags (Polymorphic, level, uniformity)