--- a/src/HOL/Tools/ATP/atp_translate.ML Sat Sep 10 00:44:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Sat Sep 10 00:44:25 2011 +0200
@@ -1257,7 +1257,7 @@
grain = Ghost_Type_Arg_Vars orelse
(exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
not (exists (type_instance ctxt T) surely_infinite_Ts orelse
- (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
+ (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts
T)))
| should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
@@ -1266,7 +1266,7 @@
grain = Ghost_Type_Arg_Vars orelse
(exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
(exists (type_generalization ctxt T) surely_finite_Ts orelse
- (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
+ (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
is_type_surely_finite ctxt T)))
| should_encode_type _ _ _ _ = false
@@ -1978,7 +1978,7 @@
case level of
Noninf_Nonmono_Types (soundness, _) =>
if exists (type_instance ctxt T) surely_infinite_Ts orelse
- member (type_aconv ctxt) maybe_finite_Ts T then
+ member (type_equiv ctxt) maybe_finite_Ts T then
mono
else if is_type_kind_of_surely_infinite ctxt soundness
surely_infinite_Ts T then
@@ -1988,14 +1988,14 @@
surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
maybe_nonmono_Ts = maybe_nonmono_Ts}
else
- {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
+ {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
surely_finite_Ts = surely_finite_Ts,
maybe_infinite_Ts = maybe_infinite_Ts,
surely_infinite_Ts = surely_infinite_Ts,
maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
| Fin_Nonmono_Types _ =>
if exists (type_instance ctxt T) surely_finite_Ts orelse
- member (type_aconv ctxt) maybe_infinite_Ts T then
+ member (type_equiv ctxt) maybe_infinite_Ts T then
mono
else if is_type_surely_finite ctxt T then
{maybe_finite_Ts = maybe_finite_Ts,
@@ -2006,7 +2006,7 @@
else
{maybe_finite_Ts = maybe_finite_Ts,
surely_finite_Ts = surely_finite_Ts,
- maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
+ maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
surely_infinite_Ts = surely_infinite_Ts,
maybe_nonmono_Ts = maybe_nonmono_Ts}
| _ => mono
--- a/src/HOL/Tools/ATP/atp_util.ML Sat Sep 10 00:44:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Sat Sep 10 00:44:25 2011 +0200
@@ -19,7 +19,7 @@
val type_instance : Proof.context -> typ -> typ -> bool
val type_generalization : Proof.context -> typ -> typ -> bool
val type_intersect : Proof.context -> typ -> typ -> bool
- val type_aconv : Proof.context -> typ * typ -> bool
+ val type_equiv : Proof.context -> typ * typ -> bool
val varify_type : Proof.context -> typ -> typ
val instantiate_type : theory -> typ -> typ -> typ -> typ
val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
@@ -123,9 +123,8 @@
Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
fun type_generalization ctxt T T' = type_instance ctxt T' T
fun type_intersect ctxt T T' =
- type_instance ctxt T T' orelse type_generalization ctxt T T'
-fun type_aconv ctxt (T, T') =
- type_instance ctxt T T' andalso type_instance ctxt T' T
+ can (Sign.typ_unify (Proof_Context.theory_of ctxt) (T, T')) (Vartab.empty, 0)
+val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
fun varify_type ctxt T =
Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
@@ -172,7 +171,7 @@
fun aux slack avoid T =
if member (op =) avoid T then
0
- else case AList.lookup (type_aconv ctxt) assigns T of
+ else case AList.lookup (type_equiv ctxt) assigns T of
SOME k => k
| NONE =>
case T of