# HG changeset patch
# User wenzelm
# Date 1723127010 -7200
# Node ID e9beaa28645dfbae431eecba48823515eeea346f
# Parent  5dec26c3688d1fd88358f2185d0bab65075c6a1b
tuned signature: more operations;

diff -r 5dec26c3688d -r e9beaa28645d src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- 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 ();
diff -r 5dec26c3688d -r e9beaa28645d src/HOL/Tools/Lifting/lifting_def.ML
--- 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
diff -r 5dec26c3688d -r e9beaa28645d src/HOL/Tools/Lifting/lifting_term.ML
--- 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
diff -r 5dec26c3688d -r e9beaa28645d src/HOL/Tools/Lifting/lifting_util.ML
--- 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 _ = []
 
diff -r 5dec26c3688d -r e9beaa28645d src/HOL/Tools/Quotient/quotient_term.ML
--- 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
diff -r 5dec26c3688d -r e9beaa28645d src/Pure/term.ML
--- 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 **)