src/HOL/Tools/ATP/atp_translate.ML
changeset 44738 1b333e4173a2
parent 44634 2ac4ff398bc3
child 44742 68e34e7f01ab
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Sep 05 17:45:37 2011 -0700
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Sep 06 09:11:08 2011 +0200
     1.3 @@ -1369,16 +1369,14 @@
     1.4  
     1.5  fun filter_type_args _ _ _ [] = []
     1.6    | filter_type_args thy s arity T_args =
     1.7 -    let val U = robust_const_type thy s in
     1.8 -      case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
     1.9 -        [] => []
    1.10 -      | res_U_vars =>
    1.11 -        let val U_args = (s, U) |> Sign.const_typargs thy in
    1.12 -          U_args ~~ T_args
    1.13 -          |> map (fn (U, T) =>
    1.14 -                     if member (op =) res_U_vars (dest_TVar U) then T
    1.15 -                     else dummyT)
    1.16 -        end
    1.17 +    let
    1.18 +      val U = robust_const_type thy s
    1.19 +      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun arity |> fst) []
    1.20 +      val U_args = (s, U) |> robust_const_typargs thy
    1.21 +    in
    1.22 +      U_args ~~ T_args
    1.23 +      |> map (fn (U, T) =>
    1.24 +                 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
    1.25      end
    1.26      handle TYPE _ => T_args
    1.27  
    1.28 @@ -1394,14 +1392,13 @@
    1.29           | SOME s'' =>
    1.30             let
    1.31               val s'' = invert_const s''
    1.32 -             fun filtered_T_args false = T_args
    1.33 -               | filtered_T_args true = filter_type_args thy s'' arity T_args
    1.34 +             fun filter_T_args false = T_args
    1.35 +               | filter_T_args true = filter_type_args thy s'' arity T_args
    1.36             in
    1.37               case type_arg_policy type_enc s'' of
    1.38 -               Explicit_Type_Args drop_args =>
    1.39 -               (name, filtered_T_args drop_args)
    1.40 +               Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
    1.41               | Mangled_Type_Args drop_args =>
    1.42 -               (mangled_const_name format type_enc (filtered_T_args drop_args)
    1.43 +               (mangled_const_name format type_enc (filter_T_args drop_args)
    1.44                                     name, [])
    1.45               | No_Type_Args => (name, [])
    1.46             end)
    1.47 @@ -1555,9 +1552,8 @@
    1.48    let
    1.49      fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
    1.50        | add (t $ u) = add t #> add u
    1.51 -      | add (Const (x as (s, _))) =
    1.52 -        if String.isPrefix skolem_const_prefix s then I
    1.53 -        else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
    1.54 +      | add (Const x) =
    1.55 +        x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
    1.56        | add (Free (s, T)) =
    1.57          if String.isPrefix polymorphic_free_prefix s then
    1.58            T |> fold_type_constrs set_insert