# HG changeset patch
# User wenzelm
# Date 1559561281 -7200
# Node ID 1514efa1e57af8ba5f64aafab3a91e20c7aa95ea
# Parent  502749883f535013110299189a043359ff0c8da9
tuned signature;

diff -r 502749883f53 -r 1514efa1e57a src/Doc/more_antiquote.ML
--- a/src/Doc/more_antiquote.ML	Mon Jun 03 11:27:23 2019 +0200
+++ b/src/Doc/more_antiquote.ML	Mon Jun 03 13:28:01 2019 +0200
@@ -20,12 +20,6 @@
 
 (* code theorem antiquotation *)
 
-fun no_vars ctxt thm =
-  let
-    val ctxt' = Variable.set_body false ctxt;
-    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
-  in thm end;
-
 val _ =
   Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>code_thms\<close> Args.term
     (fn ctxt => fn raw_const =>
@@ -38,7 +32,7 @@
           |> snd
           |> these
           |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
-          |> map (HOLogic.mk_obj_eq o no_vars ctxt o Axclass.overload ctxt);
+          |> map (HOLogic.mk_obj_eq o Variable.import_vars ctxt o Axclass.overload ctxt);
       in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end));
 
 end;
diff -r 502749883f53 -r 1514efa1e57a src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Jun 03 11:27:23 2019 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Jun 03 13:28:01 2019 +0200
@@ -557,11 +557,7 @@
     (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
     "destruct rule turned into elimination rule format" #>
   setup \<^binding>\<open>no_vars\<close>
-    (Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
-      let
-        val ctxt = Variable.set_body false (Context.proof_of context);
-        val ((_, [th']), _) = Variable.import true [th] ctxt;
-      in th' end)))
+    (Scan.succeed (Thm.rule_attribute [] (Variable.import_vars o Context.proof_of)))
     "imported schematic variables" #>
   setup \<^binding>\<open>atomize\<close>
     (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
diff -r 502749883f53 -r 1514efa1e57a src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Jun 03 11:27:23 2019 +0200
+++ b/src/Pure/variable.ML	Mon Jun 03 13:28:01 2019 +0200
@@ -79,6 +79,7 @@
   val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
   val import: bool -> thm list -> Proof.context ->
     ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
+  val import_vars: Proof.context -> thm -> thm
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val is_bound_focus: Proof.context -> bool
@@ -627,6 +628,10 @@
     val ths' = map (Thm.instantiate insts') ths;
   in ((insts', ths'), ctxt') end;
 
+fun import_vars ctxt th =
+  let val ((_, [th']), _) = ctxt |> set_body false |> import true [th];
+  in th' end;
+
 
 (* import/export *)