added export_morphism;
authorwenzelm
Fri Nov 24 22:05:18 2006 +0100 (2006-11-24)
changeset 21522bd641d927437
parent 21521 095f4963beed
child 21523 a267ecd51f90
added export_morphism;
ProofContext.init;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Fri Nov 24 22:05:17 2006 +0100
     1.2 +++ b/src/Pure/variable.ML	Fri Nov 24 22:05:18 2006 +0100
     1.3 @@ -42,6 +42,7 @@
     1.4    val exportT: Proof.context -> Proof.context -> thm list -> thm list
     1.5    val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
     1.6    val export: Proof.context -> Proof.context -> thm list -> thm list
     1.7 +  val export_morphism: Proof.context -> Proof.context -> morphism
     1.8    val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
     1.9    val import_inst: bool -> term list -> Proof.context ->
    1.10      (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
    1.11 @@ -203,7 +204,7 @@
    1.12  val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
    1.13  
    1.14  val declare_thm = Drule.fold_terms declare_internal;
    1.15 -fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
    1.16 +fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
    1.17  
    1.18  
    1.19  (* renaming term/type frees *)
    1.20 @@ -351,6 +352,12 @@
    1.21  val exportT = gen_export (rpair [] oo exportT_inst);
    1.22  val export = gen_export export_inst;
    1.23  
    1.24 +fun export_morphism inner outer =
    1.25 +  let
    1.26 +    val fact = export inner outer;
    1.27 +    val term = singleton (export_terms inner outer);
    1.28 +    val typ = Logic.type_map term;
    1.29 +  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end;
    1.30  
    1.31  
    1.32  (** import -- fix schematic type/term variables **)
    1.33 @@ -380,7 +387,7 @@
    1.34  
    1.35  fun importT ths ctxt =
    1.36    let
    1.37 -    val thy = Context.theory_of_proof ctxt;
    1.38 +    val thy = ProofContext.theory_of ctxt;
    1.39      val certT = Thm.ctyp_of thy;
    1.40      val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
    1.41      val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    1.42 @@ -395,7 +402,7 @@
    1.43  
    1.44  fun import is_open ths ctxt =
    1.45    let
    1.46 -    val thy = Context.theory_of_proof ctxt;
    1.47 +    val thy = ProofContext.theory_of ctxt;
    1.48      val cert = Thm.cterm_of thy;
    1.49      val certT = Thm.ctyp_of thy;
    1.50      val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;