--- a/src/Pure/Isar/locale.ML Mon Aug 19 18:50:45 2013 +0200
+++ b/src/Pure/Isar/locale.ML Mon Aug 19 20:37:36 2013 +0200
@@ -435,8 +435,6 @@
(** Public activation functions **)
-fun transfer_morphism thy = Morphism.thm_morphism (Thm.transfer thy);
-
fun activate_declarations dep = Context.proof_map (fn context =>
let
val thy = Context.theory_of context;
@@ -449,14 +447,15 @@
let
val thy = Context.theory_of context;
val activate =
- activate_notes Element.init (transfer_morphism o Context.theory_of) context export;
+ activate_notes Element.init
+ (Morphism.transfer_morphism o Context.theory_of) context export;
in
roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
|-> Idents.put
end;
fun init name thy =
- activate_all name thy Element.init (transfer_morphism o Context.theory_of)
+ activate_all name thy Element.init (Morphism.transfer_morphism o Context.theory_of)
(empty_idents, Context.Proof (Proof_Context.init_global thy))
|-> Idents.put |> Context.proof_of;
@@ -637,7 +636,7 @@
fun cons_elem (elem as Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
val elems =
- activate_all name thy cons_elem (K (transfer_morphism thy)) (empty_idents, [])
+ activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
|> snd |> rev;
in
Pretty.block
--- a/src/Pure/morphism.ML Mon Aug 19 18:50:45 2013 +0200
+++ b/src/Pure/morphism.ML Mon Aug 19 20:37:36 2013 +0200
@@ -33,6 +33,7 @@
val term_morphism: (term -> term) -> morphism
val fact_morphism: (thm list -> thm list) -> morphism
val thm_morphism: (thm -> thm) -> morphism
+ val transfer_morphism: theory -> morphism
val identity: morphism
val compose: morphism -> morphism -> morphism
val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
@@ -67,6 +68,7 @@
fun term_morphism term = morphism {binding = [], typ = [], term = [term], fact = []};
fun fact_morphism fact = morphism {binding = [], typ = [], term = [], fact = [fact]};
fun thm_morphism thm = morphism {binding = [], typ = [], term = [], fact = [map thm]};
+val transfer_morphism = thm_morphism o Thm.transfer;
val identity = morphism {binding = [], typ = [], term = [], fact = []};