equal
deleted
inserted
replaced
72 val get_function = NominalFunctionData.get o Context.Proof; |
72 val get_function = NominalFunctionData.get o Context.Proof; |
73 |
73 |
74 |
74 |
75 fun lift_morphism thy f = |
75 fun lift_morphism thy f = |
76 let |
76 let |
77 val term = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) |
77 fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of thy t)) |
78 in |
78 in |
79 Morphism.thm_morphism f $> Morphism.term_morphism term |
79 Morphism.thm_morphism f $> Morphism.term_morphism term |
80 $> Morphism.typ_morphism (Logic.type_map term) |
80 $> Morphism.typ_morphism (Logic.type_map term) |
81 end |
81 end |
82 |
82 |