proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
authorwenzelm
Tue Jun 04 15:11:29 2019 +0200 (6 weeks ago)
changeset 703189eff9e2dc177
parent 70317 9fced5690f4e
child 70319 34bc296374ee
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
src/HOL/Tools/Function/fun_cases.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/Function/fun_cases.ML	Tue Jun 04 13:44:59 2019 +0200
     1.2 +++ b/src/HOL/Tools/Function/fun_cases.ML	Tue Jun 04 15:11:29 2019 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4      fun mk_elim rl =
     1.5        Thm.implies_intr cprop
     1.6          (Tactic.rule_by_tactic ctxt (Inductive.mk_cases_tac ctxt) (Thm.assume cprop RS rl))
     1.7 -      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
     1.8 +      |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt);
     1.9    in
    1.10      (case get_first (try mk_elim) (flat elims) of
    1.11        SOME r => r
     2.1 --- a/src/HOL/Tools/inductive.ML	Tue Jun 04 13:44:59 2019 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Tue Jun 04 15:11:29 2019 +0200
     2.3 @@ -594,7 +594,7 @@
     2.4      fun mk_elim rl =
     2.5        Thm.implies_intr cprop
     2.6          (Tactic.rule_by_tactic ctxt (mk_cases_tac ctxt) (Thm.assume cprop RS rl))
     2.7 -      |> singleton (Variable.export (Proof_Context.augment prop ctxt) ctxt);
     2.8 +      |> singleton (Proof_Context.export (Proof_Context.augment prop ctxt) ctxt);
     2.9    in
    2.10      (case get_first (try mk_elim) elims of
    2.11        SOME r => r
    2.12 @@ -661,7 +661,7 @@
    2.13    in
    2.14      infer_instantiate ctxt' inst eq
    2.15      |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (Simplifier.full_rewrite ctxt')))
    2.16 -    |> singleton (Variable.export ctxt' ctxt)
    2.17 +    |> singleton (Proof_Context.export ctxt' ctxt)
    2.18    end
    2.19  
    2.20