--- 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;
--- 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" #>
--- 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 *)