# HG changeset patch
# User blanchet
# Date 1376967594 -7200
# Node ID 7e89edba3db64dad93dadac77a9e64d45ffcfe49
# Parent  d2afb0eb82e20434534c02a5134fc43f2d035516# Parent  6cd0feb85e35d0133b7392969ba3851c7fe13682
merged

diff -r d2afb0eb82e2 -r 7e89edba3db6 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 20 04:59:25 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 20 04:59:54 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
diff -r d2afb0eb82e2 -r 7e89edba3db6 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Aug 20 04:59:25 2013 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Aug 20 04:59:54 2013 +0200
@@ -45,15 +45,16 @@
   Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
     {target = target, is_locale = is_locale, is_class = is_class});
 
-fun is_theory lthy = Option.map #target (peek lthy) = SOME ""
-  andalso Local_Theory.level lthy = 1;
+fun is_theory lthy =
+  Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1;
 
 fun the_name lthy =
   let
     val _ = Local_Theory.assert_bottom true lthy;
-  in case Option.map #target (peek lthy) of
+  in
+    (case Option.map #target (peek lthy) of
       SOME target => target
-    | _ => error "Not in a named target"
+    | _ => error "Not in a named target")
   end;
 
 
diff -r d2afb0eb82e2 -r 7e89edba3db6 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Tue Aug 20 04:59:25 2013 +0200
+++ b/src/Pure/morphism.ML	Tue Aug 20 04:59:54 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 = []};