tuned signature;
authorwenzelm
Mon Jun 03 13:28:01 2019 +0200 (7 weeks ago)
changeset 703041514efa1e57a
parent 70303 502749883f53
child 70305 959e167798f0
tuned signature;
src/Doc/more_antiquote.ML
src/Pure/Isar/attrib.ML
src/Pure/variable.ML
     1.1 --- a/src/Doc/more_antiquote.ML	Mon Jun 03 11:27:23 2019 +0200
     1.2 +++ b/src/Doc/more_antiquote.ML	Mon Jun 03 13:28:01 2019 +0200
     1.3 @@ -20,12 +20,6 @@
     1.4  
     1.5  (* code theorem antiquotation *)
     1.6  
     1.7 -fun no_vars ctxt thm =
     1.8 -  let
     1.9 -    val ctxt' = Variable.set_body false ctxt;
    1.10 -    val ((_, [thm]), _) = Variable.import true [thm] ctxt';
    1.11 -  in thm end;
    1.12 -
    1.13  val _ =
    1.14    Theory.setup (Thy_Output.antiquotation_pretty \<^binding>\<open>code_thms\<close> Args.term
    1.15      (fn ctxt => fn raw_const =>
    1.16 @@ -38,7 +32,7 @@
    1.17            |> snd
    1.18            |> these
    1.19            |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
    1.20 -          |> map (HOLogic.mk_obj_eq o no_vars ctxt o Axclass.overload ctxt);
    1.21 +          |> map (HOLogic.mk_obj_eq o Variable.import_vars ctxt o Axclass.overload ctxt);
    1.22        in Pretty.chunks (map (Thy_Output.pretty_thm ctxt) thms) end));
    1.23  
    1.24  end;
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Jun 03 11:27:23 2019 +0200
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Jun 03 13:28:01 2019 +0200
     2.3 @@ -557,11 +557,7 @@
     2.4      (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
     2.5      "destruct rule turned into elimination rule format" #>
     2.6    setup \<^binding>\<open>no_vars\<close>
     2.7 -    (Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
     2.8 -      let
     2.9 -        val ctxt = Variable.set_body false (Context.proof_of context);
    2.10 -        val ((_, [th']), _) = Variable.import true [th] ctxt;
    2.11 -      in th' end)))
    2.12 +    (Scan.succeed (Thm.rule_attribute [] (Variable.import_vars o Context.proof_of)))
    2.13      "imported schematic variables" #>
    2.14    setup \<^binding>\<open>atomize\<close>
    2.15      (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
     3.1 --- a/src/Pure/variable.ML	Mon Jun 03 11:27:23 2019 +0200
     3.2 +++ b/src/Pure/variable.ML	Mon Jun 03 13:28:01 2019 +0200
     3.3 @@ -79,6 +79,7 @@
     3.4    val import_prf: bool -> Proofterm.proof -> Proof.context -> Proofterm.proof * Proof.context
     3.5    val import: bool -> thm list -> Proof.context ->
     3.6      ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
     3.7 +  val import_vars: Proof.context -> thm -> thm
     3.8    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
     3.9    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    3.10    val is_bound_focus: Proof.context -> bool
    3.11 @@ -627,6 +628,10 @@
    3.12      val ths' = map (Thm.instantiate insts') ths;
    3.13    in ((insts', ths'), ctxt') end;
    3.14  
    3.15 +fun import_vars ctxt th =
    3.16 +  let val ((_, [th']), _) = ctxt |> set_body false |> import true [th];
    3.17 +  in th' end;
    3.18 +
    3.19  
    3.20  (* import/export *)
    3.21