# HG changeset patch
# User wenzelm
# Date 1723125814 -7200
# Node ID 5aa376b7abb87ae224fd18df515bd47d2f0f368f
# Parent  28e8d402a9ba67db0cb8eb7af67d5568ac39d17c
tuned: more antiquotations;

diff -r 28e8d402a9ba -r 5aa376b7abb8 src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Thu Aug 08 16:03:34 2024 +0200
@@ -145,17 +145,9 @@
 
 fun try_prove_refl_rel ctxt rel =
   let
-    fun mk_ge_eq x =
-      let
-        val T = fastype_of x
-      in
-        Const (\<^const_name>\<open>less_eq\<close>, T --> T --> HOLogic.boolT) $
-          (Const (\<^const_name>\<open>HOL.eq\<close>, T)) $ x
-      end;
-    val goal = HOLogic.mk_Trueprop (mk_ge_eq rel);
-  in
-     mono_eq_prover ctxt goal
-  end;
+    val T as \<^Type>\<open>fun A _\<close> = fastype_of rel
+    val ge_eq = \<^Const>\<open>less_eq T for \<^Const>\<open>HOL.eq A\<close> rel\<close>
+  in mono_eq_prover ctxt (HOLogic.mk_Trueprop ge_eq) end;
 
 fun try_prove_reflexivity ctxt prop =
   let
@@ -223,7 +215,9 @@
 
     fun zip_transfer_rules ctxt thm =
       let
-        fun mk_POS ty = Const (\<^const_name>\<open>POS\<close>, ty --> ty --> HOLogic.boolT)
+        fun mk_POS ty =
+          let val \<^Type>\<open>fun A \<^Type>\<open>fun B bool\<close>\<close> = ty
+          in \<^Const>\<open>POS A B\<close> end
         val rel = (Thm.dest_fun2 o Thm.dest_arg o Thm.cprop_of) thm
         val typ = Thm.typ_of_cterm rel
         val POS_const = Thm.cterm_of ctxt (mk_POS typ)
@@ -279,21 +273,21 @@
 
 (* Generation of the code certificate from the rsp theorem *)
 
-fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+fun get_body_types (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) = get_body_types (U, V)
   | get_body_types (U, V)  = (U, V)
 
-fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+fun get_binder_types (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) = (T, V) :: get_binder_types (U, W)
   | get_binder_types _ = []
 
-fun get_binder_types_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [T, U]), Type ("fun", [V, W])) =
+fun get_binder_types_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun T U\<close>, \<^Type>\<open>fun V W\<close>) =
     (T, V) :: get_binder_types_by_rel S (U, W)
   | get_binder_types_by_rel _ _ = []
 
-fun get_body_type_by_rel (Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ S) (Type ("fun", [_, U]), Type ("fun", [_, V])) =
+fun get_body_type_by_rel \<^Const_>\<open>rel_fun _ _ _ _ for _ S\<close> (\<^Type>\<open>fun _ U\<close>, \<^Type>\<open>fun _ V\<close>) =
     get_body_type_by_rel S (U, V)
   | get_body_type_by_rel _ (U, V)  = (U, V)
 
-fun get_binder_rels (Const (\<^const_name>\<open>rel_fun\<close>, _) $ R $ S) = R :: get_binder_rels S
+fun get_binder_rels \<^Const_>\<open>rel_fun _ _ _ _ for R S\<close> = R :: get_binder_rels S
   | get_binder_rels _ = []
 
 fun force_rty_type ctxt rty rhs =
@@ -337,7 +331,7 @@
   let
     fun unfold_conv ctm =
       case (Thm.term_of ctm) of
-        Const (\<^const_name>\<open>map_fun\<close>, _) $ _ $ _ =>
+        \<^Const_>\<open>map_fun _ _ _ _ for _ _\<close> =>
           (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
         | _ => Conv.all_conv ctm
   in
@@ -376,9 +370,9 @@
 
 fun can_generate_code_cert quot_thm  =
   case quot_thm_rel quot_thm of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) => true
-    | Const (\<^const_name>\<open>eq_onp\<close>, _) $ _  => true
-    | _ => false
+    \<^Const_>\<open>HOL.eq _\<close> => true
+  | \<^Const_>\<open>eq_onp _ for _\<close>  => true
+  | _ => false
 
 fun generate_rep_eq ctxt def_thm rsp_thm (rty, qty) =
   let
diff -r 28e8d402a9ba -r 5aa376b7abb8 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Thu Aug 08 16:03:34 2024 +0200
@@ -179,12 +179,10 @@
 
 (** witnesses **)
 
-fun mk_undefined T = Const (\<^const_name>\<open>undefined\<close>, T);
-
 fun mk_witness quot_thm =
   let
     val wit_thm = quot_thm RS @{thm type_definition_Quotient_not_empty_witness}
-    val wit = quot_thm_rep quot_thm $ mk_undefined (quot_thm_rty_qty quot_thm |> snd)
+    val wit = quot_thm_rep quot_thm $ \<^Const>\<open>undefined \<open>quot_thm_rty_qty quot_thm |> snd\<close>\<close>
   in
     (wit, wit_thm)
   end
@@ -238,9 +236,8 @@
     fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
     fun ret_rel_conv conv ctm =
       case (Thm.term_of ctm) of
-        Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ =>
-          binop_conv2 Conv.all_conv conv ctm
-        | _ => conv ctm
+        \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> => binop_conv2 Conv.all_conv conv ctm
+      | _ => conv ctm
     fun R_conv rel_eq_onps ctxt =
       Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt
       then_conv Conv.bottom_rewrs_conv rel_eq_onps ctxt
@@ -392,7 +389,7 @@
             SOME code_dt =>
               (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_witness_of_code_dt qty_ret code_dt),
                 wit_thm_of_code_dt code_dt :: wits)
-            | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T), wits)
+            | NONE => (fold_rev (Term.lambda o curry Free Name.uu) Ts \<^Const>\<open>undefined T\<close>, wits)
       in
         @{fold_map 2} (fn Ts => fn k' => fn wits =>
           (if k = k' then (fold_rev Term.lambda xs x, wits) else gen_undef_wit Ts wits)) ctr_Tss ks []
@@ -434,13 +431,8 @@
       |>> mk_lift_const_of_lift_def (qty_isom --> qty_ret))) sel_names sel_rhs lthy5
 
     (* now we can execute the qty qty_isom isomorphism *)
-    fun mk_type_definition newT oldT RepC AbsC A =
-      let
-        val typedefC =
-          Const (\<^const_name>\<open>type_definition\<close>,
-            (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
-      in typedefC $ RepC $ AbsC $ A end;
-    val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
+    val typedef_goal =
+      \<^Const>\<open>type_definition qty_isom qty for rep_isom abs_isom \<open>HOLogic.mk_UNIV qty\<close>\<close> |>
       HOLogic.mk_Trueprop;
     fun typ_isom_tac ctxt i =
       EVERY' [ SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms type_definition_def}),
@@ -700,7 +692,7 @@
           (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq ctxt)))) ctxt
       in
         case (Thm.term_of ctm) of
-          Const (\<^const_name>\<open>rel_fun\<close>, _) $ _ $ _ => 
+          \<^Const_>\<open>rel_fun _ _ _ _ for _ _\<close> =>
             (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
           | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
       end
@@ -723,11 +715,11 @@
 
 fun rename_to_tnames ctxt term =
   let
-    fun all_typs (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (_, T, t)) = T :: all_typs t
+    fun all_typs \<^Const_>\<open>Pure.all _ for \<open>Abs (_, T, t)\<close>\<close> = T :: all_typs t
       | all_typs _ = []
 
-    fun rename (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (_, T2, t)) (new_name :: names) = 
-        (Const (\<^const_name>\<open>Pure.all\<close>, T1) $ Abs (new_name, T2, rename t names)) 
+    fun rename \<^Const_>\<open>Pure.all T1 for \<open>Abs (_, T2, t)\<close>\<close> (new_name :: names) =
+          \<^Const>\<open>Pure.all T1 for \<open>Abs (new_name, T2, rename t names)\<close>\<close>
       | rename t _ = t
 
     val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
diff -r 28e8d402a9ba -r 5aa376b7abb8 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 08 16:03:34 2024 +0200
@@ -478,12 +478,9 @@
       val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule);
       val (lhs, rhs) =
         (case concl of
-          Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
-            (lhs, rhs)
-        | Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
-            (lhs, rhs)
-        | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs =>
-            (lhs, rhs)
+          \<^Const_>\<open>less_eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
+        | \<^Const_>\<open>less_eq _ for rhs \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close>\<close> => (lhs, rhs)
+        | \<^Const_>\<open>HOL.eq _ for \<open>lhs as \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> rhs\<close> => (lhs, rhs)
         | _ => error "The rule has a wrong format.")
 
       val lhs_vars = Term.add_vars lhs []
@@ -501,10 +498,9 @@
       val rhs_args = (snd o strip_comb) rhs;
       fun check_comp t =
         (case t of
-          Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => ()
+          \<^Const_>\<open>relcompp _ _ _ for \<open>Var _\<close> \<open>Var _\<close>\<close> => ()
         | _ => error "There is an argument on the rhs that is not a composition.")
-      val _ = map check_comp rhs_args
-    in () end
+    in List.app check_comp rhs_args end
 in
 
   fun add_distr_rule distr_rule context =
@@ -513,11 +509,11 @@
       val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of distr_rule)
     in
       (case concl of
-        Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+        \<^Const_>\<open>less_eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
           add_pos_distr_rule distr_rule context
-      | Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) =>
+      | \<^Const_>\<open>less_eq _ for _ \<^Const_>\<open>relcompp _ _ _ for _ _\<close>\<close> =>
           add_neg_distr_rule distr_rule context
-      | Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ =>
+      | \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>relcompp _ _ _ for _ _\<close> _\<close> =>
           add_eq_distr_rule distr_rule context)
     end
 end
diff -r 28e8d402a9ba -r 5aa376b7abb8 src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Thu Aug 08 16:03:34 2024 +0200
@@ -81,15 +81,11 @@
     val args_fixed = (map (Term_Subst.instantiate (instT, Vars.empty))) args_subst
     val param_rel_fixed = Term_Subst.instantiate (instT, Vars.empty) param_rel_subst
     val rty = (domain_type o fastype_of) param_rel_fixed
-    val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>, 
-          (rty --> rty' --> HOLogic.boolT) --> 
-          (rty' --> qty --> HOLogic.boolT) --> 
-          rty --> qty --> HOLogic.boolT)
     val qty_name = dest_Type_name qty
     val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name)
     val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT])
     val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed)
-    val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
+    val rhs = \<^Const>\<open>relcompp rty rty' qty for param_rel_fixed fixed_crel\<close>
     val definition_term = Logic.mk_equals (lhs, rhs)
     fun note_def lthy =
       Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
@@ -151,7 +147,7 @@
           (Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt)))
   in
     case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of
-      Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
+      \<^Const_>\<open>relcompp _ _ _ for \<^Const_>\<open>HOL.eq _\<close> _\<close> =>
         let
           val thm = 
             pcr_cr_eq
@@ -164,8 +160,8 @@
         in
           (thm, lthy')
         end
-      | Const (\<^const_name>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error args_ctxt t
-      | _ => error "generate_pcr_cr_eq: implementation error"
+    | \<^Const_>\<open>relcompp _ _ _ for t _\<close> => print_generate_pcr_cr_eq_error args_ctxt t
+    | _ => error "generate_pcr_cr_eq: implementation error"
   end
 end
 
@@ -217,13 +213,12 @@
                                  Pretty.brk 1] @ 
                                  ((Pretty.commas o map (Pretty.str o quote)) extras) @
                                  [Pretty.str "."])]
-    val not_type_constr = 
-      case qty of
-         Type _ => []
-         | _ => [Pretty.block [Pretty.str "The quotient type ",
-                                Pretty.quote (Syntax.pretty_typ ctxt' qty),
-                                Pretty.brk 1,
-                                Pretty.str "is not a type constructor."]]
+    val not_type_constr =
+      if is_Type qty then []
+      else [Pretty.block [Pretty.str "The quotient type ",
+                          Pretty.quote (Syntax.pretty_typ ctxt' qty),
+                          Pretty.brk 1,
+                          Pretty.str "is not a type constructor."]]
     val errs = extra_rty_tfrees @ not_type_constr
   in
     if null errs then () else raise QUOT_ERROR errs
@@ -641,22 +636,20 @@
     (**)
     val T_def = Morphism.thm (Local_Theory.target_morphism lthy1) T_def
     (**)    
-    val quot_thm = case typedef_set of
-      Const (\<^const_name>\<open>top\<close>, _) => 
-        [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
-      | Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, _) => 
-        [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
-      | _ => 
-        [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
+    val quot_thm =
+      case typedef_set of
+        \<^Const_>\<open>top _\<close> => [typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
+      | \<^Const_>\<open>Collect _ for \<open>Abs _\<close>\<close> => [typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
+      | _ => [typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
     val (rty, qty) = quot_thm_rty_qty quot_thm
     val qty_full_name = dest_Type_name qty
     val qty_name = Binding.name (Long_Name.base_name qty_full_name)
     val qualify = Binding.qualify_name true qty_name
     val opt_reflp_thm = 
       case typedef_set of
-        Const (\<^const_name>\<open>top\<close>, _) => 
+        \<^Const_>\<open>top _\<close> =>
           SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
-        | _ =>  NONE
+      | _ =>  NONE
     val dom_thm = get_Domainp_thm quot_thm
 
     fun setup_transfer_rules_nonpar notes =
@@ -789,9 +782,9 @@
       end
   in
     case input_term of
-      (Const (\<^const_name>\<open>Quotient\<close>, _) $ _ $ _ $ _ $ _) => setup_quotient ()
-      | (Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _) => setup_typedef ()
-      | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
+      \<^Const_>\<open>Quotient _ _ for _ _ _ _\<close> => setup_quotient ()
+    | \<^Const_>\<open>type_definition _ _ for _ _ _\<close> => setup_typedef ()
+    | _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported."
   end
 
 val _ = 
@@ -830,7 +823,7 @@
                     Pretty.brk 1,
                     Thm.pretty_thm ctxt pcr_cr_eq]]
             val (pcr_const_eq, eqs) = strip_comb eq_lhs
-            fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+            fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
               | is_eq _ = false
             fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2)
               | eq_Const _ _ = false
@@ -929,14 +922,14 @@
 
 (* lifting_forget *)
 
-val monotonicity_names = [\<^const_name>\<open>right_unique\<close>, \<^const_name>\<open>left_unique\<close>, \<^const_name>\<open>right_total\<close>,
-  \<^const_name>\<open>left_total\<close>, \<^const_name>\<open>bi_unique\<close>, \<^const_name>\<open>bi_total\<close>]
-
-fun fold_transfer_rel f (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ rel $ _ $ _) = f rel
-  | fold_transfer_rel f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ 
-    (Const (\<^const_name>\<open>Domainp\<close>, _) $ rel) $ _) = f rel
-  | fold_transfer_rel f (Const (name, _) $ rel) = 
-    if member op= monotonicity_names name then f rel else f \<^term>\<open>undefined\<close>
+fun fold_transfer_rel f \<^Const_>\<open>Transfer.Rel _ _ for rel _ _\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>HOL.eq _ for \<^Const_>\<open>Domainp _ _ for rel\<close> _\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>right_unique _ _ for rel\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>left_unique _ _ for rel\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>right_total _ _ for rel\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>left_total _ _ for rel\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>bi_unique _ _ for rel\<close> = f rel
+  | fold_transfer_rel f \<^Const_>\<open>bi_total _ _ for rel\<close> = f rel
   | fold_transfer_rel f _ = f \<^term>\<open>undefined\<close>
 
 fun filter_transfer_rules_by_rel transfer_rel transfer_rules =
diff -r 28e8d402a9ba -r 5aa376b7abb8 src/HOL/Tools/Lifting/lifting_term.ML
--- a/src/HOL/Tools/Lifting/lifting_term.ML	Thu Aug 08 14:24:18 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_term.ML	Thu Aug 08 16:03:34 2024 +0200
@@ -108,8 +108,8 @@
   (case Lifting_Info.lookup_relator_distr_data ctxt s of
     SOME rel_distr_thm =>
       (case tm of
-        Const (\<^const_name>\<open>POS\<close>, _) => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
-      | Const (\<^const_name>\<open>NEG\<close>, _) => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
+        \<^Const_>\<open>POS _ _\<close> => map (Thm.transfer' ctxt) (#pos_distr_rules rel_distr_thm)
+      | \<^Const_>\<open>NEG _ _\<close> => map (Thm.transfer' ctxt) (#neg_distr_rules rel_distr_thm))
   | NONE => raise QUOT_THM_INTERNAL (Pretty.block
       [Pretty.str ("No relator distr. data for the type " ^ quote s), 
        Pretty.brk 1,
@@ -461,8 +461,8 @@
   
           fun is_POS_or_NEG ctm =
             case (head_of o Thm.term_of o Thm.dest_arg) ctm of
-              Const (\<^const_name>\<open>POS\<close>, _) => true
-            | Const (\<^const_name>\<open>NEG\<close>, _) => true
+              \<^Const_>\<open>POS _ _\<close> => true
+            | \<^Const_>\<open>NEG _ _\<close> => true
             | _ => false
   
           val inst_distr_rule = rewr_imp distr_rule ctm
@@ -480,8 +480,8 @@
   
     in
       case get_args 2 rel of
-          [Const (\<^const_name>\<open>HOL.eq\<close>, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
-          | [_, Const (\<^const_name>\<open>HOL.eq\<close>, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+          [\<^Const_>\<open>HOL.eq _\<close>, _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+          | [_, \<^Const_>\<open>HOL.eq _\<close>] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
           | [_, trans_rel] =>
             let
               val (rty', qty) = (relation_types o fastype_of) trans_rel