# HG changeset patch
# User wenzelm
# Date 1634411728 -7200
# Node ID 2f8e8dc9b5224def4439e739af52fdc4c84ccf0d
# Parent  638301b86f0a26f8658052e0fd9467de8428cf11
clarified context;

diff -r 638301b86f0a -r 2f8e8dc9b522 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Oct 16 21:14:24 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Oct 16 21:15:28 2021 +0200
@@ -86,21 +86,17 @@
     (qconst_data Morphism.identity, lthy'')
   end
 
-fun mk_readable_rsp_thm_eq tm lthy =
+fun mk_readable_rsp_thm_eq tm ctxt =
   let
-    val ctm = Thm.cterm_of lthy tm
+    val ctm = Thm.cterm_of ctxt tm
 
-    fun norm_fun_eq ctm =
-      let
-        fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
-        fun erase_quants ctm' =
-          case (Thm.term_of ctm') of
-            Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
-            | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
-              Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
-      in
-        (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
-      end
+    fun abs_conv2 cv = Conv.abs_conv (Conv.abs_conv (cv o #2) o #2) ctxt
+    fun erase_quants ctxt' ctm' =
+      case (Thm.term_of ctm') of
+        Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _ => Conv.all_conv ctm'
+        | _ => (Conv.binder_conv (erase_quants o #2) ctxt' then_conv
+          Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+    val norm_fun_eq = abs_conv2 erase_quants then_conv Thm.eta_conversion
 
     fun simp_arrows_conv ctm =
       let
@@ -117,15 +113,15 @@
       end
 
     val unfold_ret_val_invs = Conv.bottom_conv
-      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
+      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt
     val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
     val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
-    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt
     val beta_conv = Thm.beta_conversion true
     val eq_thm =
       (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
   in
-    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
+    Object_Logic.rulify ctxt (eq_thm RS Drule.equal_elim_rule2)
   end