# HG changeset patch
# User blanchet
# Date 1343371960 -7200
# Node ID 726590131ca10c61d0fab1d38970b3d496e4472e
# Parent  ba0dd46b9214632280acbce4209f96d05527f3be
bring implementation of traditional encoding in line with paper

diff -r ba0dd46b9214 -r 726590131ca1 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Jul 26 21:50:16 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jul 27 08:52:40 2012 +0200
@@ -2405,13 +2405,14 @@
     val bounds =
       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
     val bound_Ts =
-      if exists (curry (op =) dummyT) T_args then
+      case level_of_type_enc type_enc of
+        All_Types => if null T_args then replicate ary NONE else map SOME arg_Ts
+      | Undercover_Types =>
         let val cover = type_arg_cover thy NONE s ary in
           map2 (fn j => if member (op =) cover j then SOME else K NONE)
                (0 upto ary - 1) arg_Ts
         end
-      else
-        replicate ary NONE
+      | _ => replicate ary NONE
   in
     Formula (guards_sym_formula_prefix ^ s ^
              (if n > 1 then "_" ^ string_of_int j else ""), role,