added norm_export_morphism;
authorwenzelm
Mon Sep 29 10:58:04 2008 +0200 (2008-09-29)
changeset 2839672695dd4395d
parent 28395 984fcc8feb24
child 28397 389c5e494605
added norm_export_morphism;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Sep 29 10:58:03 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Sep 29 10:58:04 2008 +0200
     1.3 @@ -68,6 +68,7 @@
     1.4    val goal_export: Proof.context -> Proof.context -> thm list -> thm list
     1.5    val export: Proof.context -> Proof.context -> thm list -> thm list
     1.6    val export_morphism: Proof.context -> Proof.context -> morphism
     1.7 +  val norm_export_morphism: Proof.context -> Proof.context -> morphism
     1.8    val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
     1.9    val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
    1.10    val auto_bind_goal: term list -> Proof.context -> Proof.context
    1.11 @@ -767,6 +768,10 @@
    1.12    Assumption.export_morphism inner outer $>
    1.13    Variable.export_morphism inner outer;
    1.14  
    1.15 +fun norm_export_morphism inner outer =
    1.16 +  export_morphism inner outer $>
    1.17 +  Morphism.thm_morphism Goal.norm_result;
    1.18 +
    1.19  
    1.20  
    1.21  (** bindings **)