1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 04 13:08:44 2012 +0200
     1.3 @@ -1352,9 +1352,9 @@
     1.4     | NONE => [])
     1.5    handle TYPE _ => []
     1.6  
     1.7 -fun type_arg_cover thy s ary =
     1.8 +fun type_arg_cover thy pos s ary =
     1.9    if is_tptp_equal s then
    1.10 -    0 upto ary - 1
    1.11 +    if pos = SOME false then [] else 0 upto ary - 1
    1.12    else
    1.13      let
    1.14        val footprint = tvar_footprint thy s ary
    1.15 @@ -1431,8 +1431,9 @@
    1.16           | _ => false)
    1.17        | Undercover_Types =>
    1.18          (case (site, is_maybe_universal_var u) of
    1.19 -           (Eq_Arg _, true) => true
    1.20 -         | (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy s ary) j
    1.21 +           (Eq_Arg pos, true) => pos <> SOME false
    1.22 +         | (Arg (s, j, ary), true) =>
    1.23 +           member (op =) (type_arg_cover thy NONE s ary) j
    1.24           | _ => false)
    1.25        | _ => should_encode_type ctxt mono level T
    1.26      end
    1.27 @@ -1989,15 +1990,15 @@
    1.28      (is_tptp_equal s andalso member (op =) tms (ATerm ((name, []), [])))
    1.29    | is_var_positively_naked_in_term _ _ _ _ = true
    1.30  
    1.31 -fun is_var_positively_naked_or_undercover_in_term thy name pos tm accum =
    1.32 -  is_var_positively_naked_in_term name pos tm accum orelse
    1.33 +fun is_var_undercover_in_term thy name pos tm accum =
    1.34 +  accum orelse
    1.35    let
    1.36      val var = ATerm ((name, []), [])
    1.37      fun is_undercover (ATerm (_, [])) = false
    1.38        | is_undercover (ATerm (((s, _), _), tms)) =
    1.39          let
    1.40            val ary = length tms
    1.41 -          val cover = type_arg_cover thy s ary
    1.42 +          val cover = type_arg_cover thy pos s ary
    1.43          in
    1.44            exists (fn (j, tm) => tm = var andalso member (op =) cover j)
    1.45                   (0 upto ary - 1 ~~ tms) orelse
    1.46 @@ -2013,8 +2014,7 @@
    1.47       | Nonmono_Types (_, Non_Uniform) =>
    1.48         formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.49       | Undercover_Types =>
    1.50 -       formula_fold pos (is_var_positively_naked_or_undercover_in_term thy name)
    1.51 -                    phi false
    1.52 +       formula_fold pos (is_var_undercover_in_term thy name) phi false
    1.53       | _ => false)
    1.54    | should_guard_var_in_formula _ _ _ _ _ _ = true
    1.55  
    1.56 @@ -2420,7 +2420,7 @@
    1.57        bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
    1.58      val bound_Ts =
    1.59        if exists (curry (op =) dummyT) T_args then
    1.60 -        let val cover = type_arg_cover thy s ary in
    1.61 +        let val cover = type_arg_cover thy NONE s ary in
    1.62            map2 (fn j => if member (op =) cover j then SOME else K NONE)
    1.63                 (0 upto ary - 1) arg_Ts
    1.64          end
    1.65 @@ -2462,7 +2462,7 @@
    1.66          let
    1.67            val tagged_bounds =
    1.68              if level = Undercover_Types then
    1.69 -              let val cover = type_arg_cover thy s ary in
    1.70 +              let val cover = type_arg_cover thy NONE s ary in
    1.71                  map2 (fn (j, arg_T) => member (op =) cover j ? tag_with arg_T)
    1.72                       (0 upto ary - 1 ~~ arg_Ts) bounds
    1.73                end