# HG changeset patch
# User wenzelm
# Date 1635527844 -7200
# Node ID 9a1f4a7ddf9ef7428bba6dc14c4220df73aa5c43
# Parent  e6f0c9bf966c1807795a2bb83c8ef78f76ce4130
clarified antiquotations;

diff -r e6f0c9bf966c -r 9a1f4a7ddf9e src/HOL/Analysis/normarith.ML
--- a/src/HOL/Analysis/normarith.ML	Fri Oct 29 15:09:46 2021 +0200
+++ b/src/HOL/Analysis/normarith.ML	Fri Oct 29 19:17:24 2021 +0200
@@ -258,10 +258,6 @@
   then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;
 
 local
- val pth_zero = @{thm norm_zero}
- val tv_n =
-  (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
-    pth_zero
  val concl = Thm.dest_arg o Thm.cprop_of
  fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
   let
@@ -323,9 +319,9 @@
         (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
 
   in fst (RealArith.real_linear_prover translator
-        (map (fn t =>
-          Drule.instantiate_normalize (TVars.make [(tv_n, Thm.ctyp_of_cterm t)], Vars.empty) pth_zero)
-            zerodests,
+        (zerodests |> map (fn t =>
+          \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm t\<close> in
+            lemma \<open>norm (0::'a::real_normed_vector) = 0\<close> by simp\<close>),
         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 norm_canon_conv ctxt) then_conv