clarified antiquotations;
authorwenzelm
Thu, 28 Oct 2021 20:05:18 +0200
changeset 74996 3ef6e38c9847
parent 74995 cce64b47d13a
child 74997 87fc10f5826c
clarified antiquotations;
src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Thu Oct 28 20:04:06 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Thu Oct 28 20:05:18 2021 +0200
@@ -66,14 +66,16 @@
        val n = vs |> length
                |> HOLogic.mk_number \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
-       val s = vs
+       val ss = vs
                |> map lookup_splitting
                |> HOLogic.mk_list \<^Type>\<open>nat\<close>
                |> Thm.cterm_of ctxt
      in
-       (resolve_tac ctxt [Thm.instantiate (TVars.empty,
-           Vars.make [(\<^var>\<open>?n::nat\<close>, n), (\<^var>\<open>?prec::nat\<close>, p), (\<^var>\<open>?ss::nat list\<close>, s)])
-            @{thm approx_form}] i
+       (resolve_tac ctxt [
+          \<^instantiate>\<open>n and prec = p and ss in
+            lemma (schematic)
+              \<open>n = length xs \<Longrightarrow> approx_form prec f (replicate n None) ss \<Longrightarrow> interpret_form f xs\<close>
+              by (rule approx_form)\<close>] i
         THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st
      end
 
@@ -87,9 +89,10 @@
        val s = vs |> map lookup_splitting |> hd
             |> Thm.cterm_of ctxt
      in
-       resolve_tac ctxt [Thm.instantiate (TVars.empty,
-            Vars.make [(\<^var>\<open>?s::nat\<close>, s), (\<^var>\<open>?t::nat\<close>, t), (\<^var>\<open>?prec::nat\<close>, p)])
-            @{thm approx_tse_form}] i st
+       resolve_tac ctxt [
+         \<^instantiate>\<open>s and t and prec = p in
+           lemma (schematic) "approx_tse_form prec t s f \<Longrightarrow> interpret_form f [x]"
+            by (rule approx_tse_form)\<close>] i st
      end
   end