diff -r 6d2af424d0f8 -r e9c90516bc0d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Feb 05 17:43:15 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Feb 06 23:01:01 2012 +0100
@@ -72,7 +72,7 @@
   val app_op_name : string
   val type_guard_name : string
   val type_tag_name : string
-  val simple_type_prefix : string
+  val native_type_prefix : string
   val prefixed_predicator_name : string
   val prefixed_app_op_name : string
   val prefixed_type_tag_name : string
@@ -145,7 +145,7 @@
 val tfree_prefix = "t_"
 val const_prefix = "c_"
 val type_const_prefix = "tc_"
-val simple_type_prefix = "s_"
+val native_type_prefix = "n_"
 val class_prefix = "cl_"
 
 (* Freshness almost guaranteed! *)
@@ -631,7 +631,7 @@
        |> try_nonmono (curry Noninf_Nonmono_Types strictness) queries)
   |> (fn (poly, (level, core)) =>
          case (core, (poly, level)) of
-           ("simple", (SOME poly, _)) =>
+           ("native", (SOME poly, _)) =>
            (case (poly, level) of
               (Polymorphic, All_Types) =>
               Simple_Types (First_Order, Polymorphic, All_Types)
@@ -641,7 +641,7 @@
               else
                 raise Same.SAME
             | _ => raise Same.SAME)
-         | ("simple_higher", (SOME poly, _)) =>
+         | ("native_higher", (SOME poly, _)) =>
            (case (poly, level) of
               (Polymorphic, All_Types) =>
               Simple_Types (Higher_Order, Polymorphic, All_Types)
@@ -889,17 +889,17 @@
 fun mangled_type format type_enc =
   generic_mangled_type_name fst o ho_term_from_typ format type_enc
 
-fun make_simple_type s =
+fun make_native_type s =
   if s = tptp_bool_type orelse s = tptp_fun_type orelse
      s = tptp_individual_type then
     s
   else
-    simple_type_prefix ^ ascii_of s
+    native_type_prefix ^ ascii_of s
 
 fun ho_type_from_ho_term type_enc pred_sym ary =
   let
     fun to_mangled_atype ty =
-      AType ((make_simple_type (generic_mangled_type_name fst ty),
+      AType ((make_native_type (generic_mangled_type_name fst ty),
               generic_mangled_type_name snd ty), [])
     fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
       | to_poly_atype _ = raise Fail "unexpected type abstraction"