added export_morphism;
authorwenzelm
Fri Nov 24 22:05:13 2006 +0100 (2006-11-24)
changeset 21517b165c9120702
parent 21516 c2a116a2c4fd
child 21518 571b8cd087f8
added export_morphism;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Fri Nov 24 22:05:12 2006 +0100
     1.2 +++ b/src/Pure/assumption.ML	Fri Nov 24 22:05:13 2006 +0100
     1.3 @@ -18,6 +18,7 @@
     1.4    val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
     1.5    val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
     1.6    val export: bool -> Proof.context -> Proof.context -> thm -> thm
     1.7 +  val export_morphism: Proof.context -> Proof.context -> morphism
     1.8  end;
     1.9  
    1.10  structure Assumption: ASSUMPTION =
    1.11 @@ -104,4 +105,11 @@
    1.12      #> norm_hhf_protect
    1.13    end;
    1.14  
    1.15 +fun export_morphism inner outer =
    1.16 +  let
    1.17 +    val thm = export false inner outer;
    1.18 +    fun term t = Drule.term_rule (ProofContext.theory_of inner (*delayed until now*)) thm t;
    1.19 +    val typ = Logic.type_map term;
    1.20 +  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
    1.21 +
    1.22  end;