src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 36170 0cdb76723c88
parent 36169 27b1cc58715e
child 36230 43d10a494c91
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 16 14:48:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 16 15:49:13 2010 +0200
     1.3 @@ -79,15 +79,15 @@
     1.4  
     1.5  fun hol_term_to_fol_FO tm =
     1.6    case strip_combterm_comb tm of
     1.7 -      (CombConst(c,_,tys), tms) =>
     1.8 +      (CombConst ((c, _), _, tys), tms) =>
     1.9          let val tyargs = map hol_type_to_fol tys
    1.10              val args   = map hol_term_to_fol_FO tms
    1.11          in Metis.Term.Fn (c, tyargs @ args) end
    1.12 -    | (CombVar(v,_), []) => Metis.Term.Var v
    1.13 +    | (CombVar ((v, _), _), []) => Metis.Term.Var v
    1.14      | _ => error "hol_term_to_fol_FO";
    1.15  
    1.16 -fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
    1.17 -  | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
    1.18 +fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
    1.19 +  | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
    1.20        Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
    1.21    | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
    1.22         Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
    1.23 @@ -95,26 +95,26 @@
    1.24  (*The fully-typed translation, to avoid type errors*)
    1.25  fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
    1.26  
    1.27 -fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
    1.28 -  | hol_term_to_fol_FT (CombConst(a, ty, _)) =
    1.29 +fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
    1.30 +  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
    1.31        wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
    1.32    | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
    1.33         wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
    1.34                    type_of_combterm tm);
    1.35  
    1.36  fun hol_literal_to_fol FO (Literal (pol, tm)) =
    1.37 -      let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
    1.38 +      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
    1.39            val tylits = if p = "equal" then [] else map hol_type_to_fol tys
    1.40            val lits = map hol_term_to_fol_FO tms
    1.41        in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
    1.42    | hol_literal_to_fol HO (Literal (pol, tm)) =
    1.43       (case strip_combterm_comb tm of
    1.44 -          (CombConst("equal",_,_), tms) =>
    1.45 +          (CombConst(("equal", _), _, _), tms) =>
    1.46              metis_lit pol "=" (map hol_term_to_fol_HO tms)
    1.47          | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
    1.48    | hol_literal_to_fol FT (Literal (pol, tm)) =
    1.49       (case strip_combterm_comb tm of
    1.50 -          (CombConst("equal",_,_), tms) =>
    1.51 +          (CombConst(("equal", _), _, _), tms) =>
    1.52              metis_lit pol "=" (map hol_term_to_fol_FT tms)
    1.53          | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
    1.54