Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more accurate treatment of context;
authorwenzelm
Tue, 19 Oct 2021 14:41:29 +0200
changeset 74544 9864ab4c20ce
parent 74541 2ff001a8c9f2
child 74545 6c123914883a
more accurate treatment of context;
src/HOL/Analysis/normarith.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle