summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Mon, 03 Jun 2019 20:09:43 +0200 | |

changeset 70310 | c82f59c47aaf |

parent 70309 | f9fd15d3cfac |

child 70311 | e49bf4ebf330 |

clarified transfer_morphism: implicit join_certificate, e.g. relevant for complex cascades of morphisms such as class locale interpretation;

src/Pure/morphism.ML | file | annotate | diff | comparison | revisions | |

src/Pure/thm.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/morphism.ML Mon Jun 03 17:01:28 2019 +0200 +++ b/src/Pure/morphism.ML Mon Jun 03 20:09:43 2019 +0200 @@ -125,7 +125,7 @@ fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]}; fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]}; -val transfer_morphism = thm_morphism "transfer" o Thm.transfer; +val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer; val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; val transfer_morphism'' = transfer_morphism o Context.theory_of;

--- a/src/Pure/thm.ML Mon Jun 03 17:01:28 2019 +0200 +++ b/src/Pure/thm.ML Mon Jun 03 20:09:43 2019 +0200 @@ -89,6 +89,7 @@ val transfer: theory -> thm -> thm val transfer': Proof.context -> thm -> thm val transfer'': Context.generic -> thm -> thm + val join_transfer: theory -> thm -> thm val renamed_prop: term -> thm -> thm val weaken: cterm -> thm -> thm val weaken_sorts: sort list -> cterm -> cterm @@ -530,6 +531,10 @@ val transfer' = transfer o Proof_Context.theory_of; val transfer'' = transfer o Context.theory_of; +fun join_transfer thy th = + if Context.subthy_id (Context.theory_id thy, theory_id th) then th + else transfer thy th; + (* matching *)