# HG changeset patch
# User wenzelm
# Date 1634647289 -7200
# Node ID 9864ab4c20cefc0b0bb2b98db24e9548310a7b53
# Parent  2ff001a8c9f22f0def7b15c441dd6ea75098f0a5
more accurate treatment of context;

diff -r 2ff001a8c9f2 -r 9864ab4c20ce src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Mon Oct 18 18:33:46 2021 +0200
+++ b/src/HOL/Analysis/normarith.ML	Tue Oct 19 14:41:29 2021 +0200
@@ -325,9 +325,9 @@
         (map (fn t =>
           Drule.instantiate_normalize (TVars.make [(tv_n, Thm.ctyp_of_cterm t)], Vars.empty) pth_zero)
             zerodests,
-        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv norm_canon_conv ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) ges',
-        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
+        map (fconv_rule (try_conv (Conv.top_sweep_conv norm_canon_conv ctxt) then_conv
                        arg_conv (arg_conv real_poly_conv))) gts))
   end
 in val real_vector_combo_prover = real_vector_combo_prover