src/HOL/Tools/Quotient/quotient_term.ML

 datatype flag = AbsF | RepF
 
 fun negF AbsF = RepF
   | negF RepF = AbsF
 
-fun is_identity (Const (\<^const_name>\<open>id\<close>, _)) = true
+fun is_identity \<^Const_>\<open>id _\<close> = true
   | is_identity _ = false
-
-fun mk_identity ty = Const (\<^const_name>\<open>id\<close>, ty --> ty)
 
 fun mk_fun_compose flag (trm1, trm2) =
   case flag of
     AbsF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm1 $ trm2
   | RepF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm2 $ trm1

         else 
           raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
       end
   in
     if rty = qty
-    then mk_identity rty
+    then \<^Const>\<open>id rty\<close>
     else
       case (rty, qty) of
         (Type (s, tys), Type (s', tys')) =>
           if s = s'
           then

                     end
                 end
             end
       | (TFree x, TFree x') =>
           if x = x'
-          then mk_identity rty
+          then \<^Const>\<open>id rty\<close>
           else raise (LIFT_MATCH "absrep_fun (frees)")
       | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
       | _ => raise (LIFT_MATCH "absrep_fun (default)")
   end
 

     val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
   in
     map_types (Envir.subst_type ty_inst) trm
   end
 
-fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true
+fun is_eq \<^Const_>\<open>HOL.eq _\<close> = true
   | is_eq _ = false
 
 fun mk_rel_compose (trm1, trm2) =
   Const (\<^const_abbrev>\<open>rel_conj\<close>, dummyT) $ trm1 $ trm2