src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 38864 4abe644fcea5
parent 38748 69fea359d3f8
child 38994 7c655a491bce
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4  
     1.5  fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
     1.6  
     1.7 -fun smart_invert_const "fequal" = @{const_name "op ="}
     1.8 +fun smart_invert_const "fequal" = @{const_name HOL.eq}
     1.9    | smart_invert_const s = invert_const s
    1.10  
    1.11  fun hol_type_from_metis_term _ (Metis.Term.Var v) =
    1.12 @@ -264,7 +264,7 @@
    1.13              end
    1.14          | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
    1.15        and applic_to_tt ("=",ts) =
    1.16 -            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
    1.17 +            Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
    1.18          | applic_to_tt (a,ts) =
    1.19              case strip_prefix_and_unascii const_prefix a of
    1.20                  SOME b =>
    1.21 @@ -311,7 +311,7 @@
    1.22                    SOME w =>  mk_var(w, dummyT)
    1.23                  | NONE   => mk_var(v, dummyT))
    1.24          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
    1.25 -            Const (@{const_name "op ="}, HOLogic.typeT)
    1.26 +            Const (@{const_name HOL.eq}, HOLogic.typeT)
    1.27          | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
    1.28             (case strip_prefix_and_unascii const_prefix x of
    1.29                  SOME c => Const (smart_invert_const c, dummyT)
    1.30 @@ -325,7 +325,7 @@
    1.31              cvt tm1 $ cvt tm2
    1.32          | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
    1.33          | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
    1.34 -            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
    1.35 +            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
    1.36          | cvt (t as Metis.Term.Fn (x, [])) =
    1.37             (case strip_prefix_and_unascii const_prefix x of
    1.38                  SOME c => Const (smart_invert_const c, dummyT)
    1.39 @@ -480,7 +480,7 @@
    1.40        val c_t = cterm_incr_types thy refl_idx i_t
    1.41    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
    1.42  
    1.43 -fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
    1.44 +fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
    1.45    | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
    1.46    | get_ty_arg_size _ _ = 0;
    1.47  
    1.48 @@ -529,13 +529,13 @@
    1.49                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
    1.50                        " fol-term: " ^ Metis.Term.toString t)
    1.51        fun path_finder FO tm ps _ = path_finder_FO tm ps
    1.52 -        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
    1.53 +        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
    1.54               (*equality: not curried, as other predicates are*)
    1.55               if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
    1.56               else path_finder_HO tm (p::ps)        (*1 selects second operand*)
    1.57          | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
    1.58               path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
    1.59 -        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
    1.60 +        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
    1.61                              (Metis.Term.Fn ("=", [t1,t2])) =
    1.62               (*equality: not curried, as other predicates are*)
    1.63               if p=0 then path_finder_FT tm (0::1::ps)