# HG changeset patch
# User wenzelm
# Date 1723290548 -7200
# Node ID d2920ff628274275eedf54ffb6020fc9b8f56646
# Parent  3d99104b4b9b51a3831335f13fdca46c87c5674b
tuned: eliminate odd clones;

diff -r 3d99104b4b9b -r d2920ff62827 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 13:42:27 2024 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 10 13:49:08 2024 +0200
@@ -37,9 +37,6 @@
   |> Simplifier.set_subgoaler asm_simp_tac
   |> Simplifier.set_mksimps (mksimps [])
 
-(* composition of two theorems, used in maps *)
-fun OF1 thm1 thm2 = thm2 RS thm1
-
 fun atomize_thm ctxt thm =
   let
     val thm' = Thm.legacy_freezeT (Thm.forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? no! *)
@@ -135,13 +132,13 @@
 *)
 
 fun reflp_get ctxt =
-  map_filter (fn th => if Thm.no_prems th then SOME (OF1 @{thm equivp_reflp} th) else NONE
+  map_filter (fn th => if Thm.no_prems th then SOME (th RS @{thm equivp_reflp}) else NONE
     handle THM _ => NONE) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
 
 val eq_imp_rel = @{lemma "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" by (simp add: equivp_reflp)}
 
 fun eq_imp_rel_get ctxt =
-  map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
+  map (fn th => th RS eq_imp_rel) (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>quot_equiv\<close>))
 
 val regularize_simproc =
   \<^simproc_setup>\<open>passive regularize