# HG changeset patch
# User ballarin
# Date 1227546172 -3600
# Node ID 141ed00656aefcb7a969ac009640ab658b18fdc3
# Parent  9ff624bd4fe1b5effee6fb74a105fedade61a422
Generalised activation code.

diff -r 9ff624bd4fe1 -r 141ed00656ae src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Mon Nov 24 14:23:04 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Mon Nov 24 18:02:52 2008 +0100
@@ -37,9 +37,11 @@
   val add_declaration: string -> declaration -> Proof.context -> Proof.context
 
   (* Activate locales *)
-  val activate_declarations: string -> Morphism.morphism -> theory -> identifiers ->
-    Proof.context -> identifiers * Proof.context
-  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a
+  val activate_declarations: theory -> string * Morphism.morphism ->
+    identifiers * Proof.context -> identifiers * Proof.context
+  val activate_facts: theory -> string * Morphism.morphism ->
+    identifiers * Proof.context -> identifiers * Proof.context
+(*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
   val init: string -> theory -> Proof.context
 
   (* Diagnostic *)
@@ -204,12 +206,13 @@
       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
   end;
 
-fun activate_declarations name morph thy marked ctxt =
+fun activate_declarations thy (name, morph) (marked, ctxt) =
   let
     val name' = intern thy name;
     val Loc {dependencies, ...} = the_locale thy name';
     val (dependencies', marked) =
-      roundup thy ((name', morph) :: map fst dependencies, marked);
+      roundup thy ((name', morph) ::
+        map (fn ((n, morph'), _) => (n, morph' $> morph)) dependencies, marked);
   in
     (marked, ctxt |> fold_rev (activate_decls thy) dependencies')
   end;
@@ -225,6 +228,17 @@
     fold_rev activate notes input
   end;
 
+fun activate_facts_intern thy activ_elem (name, morph) (marked, ctxt) =
+  let
+    val name' = intern thy name;
+    val Loc {dependencies, ...} = the_locale thy name';
+    val (dependencies', marked) =
+      roundup thy ((name', morph) ::
+        map (fn ((n, morph'), _) => (n, morph' $> morph)) dependencies, marked);
+  in
+    (marked, ctxt |> fold_rev (activate_notes activ_elem thy) dependencies')
+  end;
+
 fun activate name thy activ_elem input =
   let
     val name' = intern thy name;
@@ -240,7 +254,7 @@
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
         else I) |>
-      fold_rev (activate_notes activ_elem thy) dependencies'
+      pair empty |> activate_facts_intern thy activ_elem (name', Morphism.identity) |> snd
   end;
 
 local
@@ -272,6 +286,8 @@
 
 in
 
+fun activate_facts thy dep = activate_facts_intern thy init_elem dep;
+
 fun init name thy = activate name thy init_elem (ProofContext.init thy);
 
 fun print_locale thy show_facts name =