--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Thu Aug 08 16:23:30 2024 +0200
@@ -998,9 +998,6 @@
val is_valid_case_argumentT = not o member (op =) [Y, ssig_T];
- fun is_same_type_constr (Type (s, _)) (Type (s', _)) = (s = s')
- | is_same_type_constr _ _ = false;
-
exception NO_ENCAPSULATION of unit;
val parametric_consts = Unsynchronized.ref [];
@@ -1064,7 +1061,7 @@
CLeaf $ t
else if T = YpreT then
it $ t
- else if is_nested_type T andalso is_same_type_constr T U then
+ else if is_nested_type T andalso eq_Type_name (T, U) then
explore_nested lthy encapsulate params t
else
raise NO_ENCAPSULATION ();
--- a/src/HOL/Tools/Lifting/lifting_def.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Thu Aug 08 16:23:30 2024 +0200
@@ -469,7 +469,7 @@
local
fun no_no_code ctxt (rty, qty) =
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
else
if Term.is_Type qty then
--- a/src/HOL/Tools/Lifting/lifting_term.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Thu Aug 08 16:23:30 2024 +0200
@@ -450,9 +450,6 @@
val tm = Thm.term_of ctm
val rel = (hd o get_args 2) tm
- fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
- | same_constants _ _ = false
-
fun prove_extra_assms ctxt ctm distr_rule =
let
fun prove_assm assm =
@@ -486,7 +483,7 @@
let
val (rty', qty) = (relation_types o fastype_of) trans_rel
in
- if same_type_constrs (rty', qty) then
+ if eq_Type_name (rty', qty) then
let
val distr_rules = get_rel_distr_rules ctxt0 (dest_Type_name rty') (head_of tm)
val distr_rule = get_first (prove_extra_assms ctxt0 ctm) distr_rules
@@ -502,7 +499,7 @@
val pcrel_def = get_pcrel_def quotients ctxt0 (dest_Type_name qty)
val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
in
- if same_constants pcrel_const (head_of trans_rel) then
+ if eq_Const_name (pcrel_const, head_of trans_rel) then
let
val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
@@ -540,7 +537,7 @@
let
val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm)
in
- if same_type_constrs (rty, qty) then
+ if eq_Type_name (rty, qty) then
if forall op= (Targs rty ~~ Targs qty) then
Conv.all_conv ctm
else
--- a/src/HOL/Tools/Lifting/lifting_util.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Thu Aug 08 16:23:30 2024 +0200
@@ -24,7 +24,6 @@
val get_args: int -> term -> term list
val strip_args: int -> term -> term
val all_args_conv: conv -> conv
- val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
val is_rel_fun: term -> bool
@@ -100,9 +99,6 @@
fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
- | same_type_constrs _ = false
-
fun Targs (Type (_, args)) = args
| Targs _ = []
--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Aug 08 16:23:30 2024 +0200
@@ -607,8 +607,8 @@
| (_, Const _) =>
let
val thy = Proof_Context.theory_of ctxt
- fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T'
- | same_const _ _ = false
+ fun same_const t u =
+ eq_Const_name (t, u) andalso matches_typ ctxt (dest_Const_type t) (dest_Const_type u)
in
if same_const rtrm qtrm then rtrm
else
--- a/src/Pure/term.ML Thu Aug 08 16:21:48 2024 +0200
+++ b/src/Pure/term.ML Thu Aug 08 16:23:30 2024 +0200
@@ -37,6 +37,7 @@
val is_Type: typ -> bool
val is_TFree: typ -> bool
val is_TVar: typ -> bool
+ val eq_Type_name: typ * typ -> bool
val dest_Type: typ -> string * typ list
val dest_Type_name: typ -> string
val dest_Type_args: typ -> typ list
@@ -46,6 +47,7 @@
val is_Const: term -> bool
val is_Free: term -> bool
val is_Var: term -> bool
+ val eq_Const_name: term * term -> bool
val dest_Const: term -> string * typ
val dest_Const_name: term -> string
val dest_Const_type: term -> typ
@@ -280,6 +282,9 @@
fun is_TVar (TVar _) = true
| is_TVar _ = false;
+fun eq_Type_name (Type (a, _), Type (b, _)) = a = b
+ | eq_Type_name _ = false;
+
(** Destructors **)
@@ -310,6 +315,9 @@
fun is_Var (Var _) = true
| is_Var _ = false;
+fun eq_Const_name (Const (a, _), Const (b, _)) = a = b
+ | eq_Const_name _ = false;
+
(** Destructors **)