src/HOL/Tools/Sledgehammer/metis_translate.ML
changeset 39720 0b93a954da4f
parent 39499 40bf0f66b994
child 39886 8a9f0c97d550
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_translate.ML	Mon Sep 27 09:17:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_translate.ML	Mon Sep 27 10:44:08 2010 +0200
     1.3 @@ -554,7 +554,8 @@
     1.4         Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
     1.5  
     1.6  (*The fully-typed translation, to avoid type errors*)
     1.7 -fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
     1.8 +fun wrap_type (tm, ty) =
     1.9 +  Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
    1.10  
    1.11  fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
    1.12    | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =