--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Aug 28 16:14:32 2010 +0200
@@ -224,7 +224,7 @@
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
-fun smart_invert_const "fequal" = @{const_name "op ="}
+fun smart_invert_const "fequal" = @{const_name HOL.eq}
| smart_invert_const s = invert_const s
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
@@ -264,7 +264,7 @@
end
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
- Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
+ Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
| applic_to_tt (a,ts) =
case strip_prefix_and_unascii const_prefix a of
SOME b =>
@@ -311,7 +311,7 @@
SOME w => mk_var(w, dummyT)
| NONE => mk_var(v, dummyT))
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
- Const (@{const_name "op ="}, HOLogic.typeT)
+ Const (@{const_name HOL.eq}, HOLogic.typeT)
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -325,7 +325,7 @@
cvt tm1 $ cvt tm2
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
- list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
+ list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
| cvt (t as Metis.Term.Fn (x, [])) =
(case strip_prefix_and_unascii const_prefix x of
SOME c => Const (smart_invert_const c, dummyT)
@@ -480,7 +480,7 @@
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
-fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
+fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*)
| get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0;
@@ -529,13 +529,13 @@
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis.Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
- | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
+ | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
| path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
- | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
+ | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
(Metis.Term.Fn ("=", [t1,t2])) =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_FT tm (0::1::ps)