src/HOL/Tools/Metis/metis_translate.ML
changeset 41138 eb80538166b6
parent 40259 c0e34371c2e2
child 41139 cb1cbae54dbf
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4       tfrees: type_literal list,
     1.5       old_skolems: (string * term) list}
     1.6  
     1.7 -  val type_wrapper_name : string
     1.8 +  val type_tag_name : string
     1.9    val bound_var_prefix : string
    1.10    val schematic_var_prefix: string
    1.11    val fixed_var_prefix: string
    1.12 @@ -82,7 +82,7 @@
    1.13  structure Metis_Translate : METIS_TRANSLATE =
    1.14  struct
    1.15  
    1.16 -val type_wrapper_name = "ti"
    1.17 +val type_tag_name = "ty"
    1.18  
    1.19  val bound_var_prefix = "B_"
    1.20  val schematic_var_prefix = "V_"
    1.21 @@ -580,15 +580,16 @@
    1.22         Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    1.23  
    1.24  (*The fully-typed translation, to avoid type errors*)
    1.25 -fun wrap_type (tm, ty) =
    1.26 -  Metis_Term.Fn (type_wrapper_name, [tm, metis_term_from_combtyp ty])
    1.27 +fun tag_with_type tm ty =
    1.28 +  Metis_Term.Fn (type_tag_name, [tm, metis_term_from_combtyp ty])
    1.29  
    1.30 -fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
    1.31 -  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
    1.32 -      wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
    1.33 -  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
    1.34 -       wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
    1.35 -                  combtyp_of tm)
    1.36 +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) =
    1.37 +    tag_with_type (Metis_Term.Var s) ty
    1.38 +  | hol_term_to_fol_FT (CombConst ((a, _), ty, _)) =
    1.39 +    tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty
    1.40 +  | hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) =
    1.41 +    tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2]))
    1.42 +                  (combtyp_of tm)
    1.43  
    1.44  fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
    1.45        let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm