paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
authorblanchet
Mon Oct 04 20:55:55 2010 +0200 (2010-10-04)
changeset 399396e9aff5ee9b5
parent 39938 0a2091f86eb4
child 39940 1f01c9b2b76b
paramify new skolems just like old ones (cf. reveal_old_skolem_terms)
src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Oct 04 18:31:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Mon Oct 04 20:55:55 2010 +0200
     1.3 @@ -121,10 +121,12 @@
     1.4                      val nterms = length ts - ntypes
     1.5                      val tts = map tm_to_tt ts
     1.6                      val tys = types_of (List.take(tts,ntypes))
     1.7 -                    val t = if String.isPrefix new_skolem_const_prefix c then
     1.8 -                              Var (new_skolem_var_from_const c, tl tys ---> hd tys)
     1.9 -                            else
    1.10 -                              Const (c, dummyT)
    1.11 +                    val t =
    1.12 +                      if String.isPrefix new_skolem_const_prefix c then
    1.13 +                        Var (new_skolem_var_from_const c,
    1.14 +                             Type_Infer.paramify_vars (tl tys ---> hd tys))
    1.15 +                      else
    1.16 +                        Const (c, dummyT)
    1.17                    in if length tys = ntypes then
    1.18                           apply_list t nterms (List.drop(tts,ntypes))
    1.19                       else