# HG changeset patch
# User wenzelm
# Date 1238342774 -7200
# Node ID 9960ff945c521f29856cdf39be50b5218e5e35de
# Parent  fcd49e9325034d7c5bf98bbc257f1d0a8085915d
simplified Element.activate(_i): singleton version;

diff -r fcd49e932503 -r 9960ff945c52 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Mar 29 17:47:58 2009 +0200
+++ b/src/Pure/Isar/element.ML	Sun Mar 29 18:06:14 2009 +0200
@@ -61,8 +61,8 @@
   val eq_morphism: theory -> thm list -> morphism
   val transfer_morphism: theory -> morphism
   val init: context_i -> Context.generic -> Context.generic
-  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
-  val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
+  val activate_i: context_i -> Proof.context -> context_i * Proof.context
+  val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
 end;
 
 structure Element: ELEMENT =
@@ -516,30 +516,20 @@
 
 (* activate *)
 
-local
-
-fun gen_activate prep_facts raw_elems ctxt =
+fun activate_i elem ctxt =
   let
-    fun activate elem ctxt' =
-      let val elem' = map_ctxt_attrib Args.assignable (prep_facts ctxt' elem)
-      in (elem', Context.proof_map (init elem') ctxt') end;
-    val (elems, ctxt') = fold_map activate raw_elems ctxt;
-  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
+    val elem' = map_ctxt_attrib Args.assignable elem;
+    val ctxt' = Context.proof_map (init elem') ctxt;
+  in (map_ctxt_attrib Args.closure elem', ctxt') end;
 
-fun prep_facts ctxt =
-  map_ctxt
+fun activate raw_elem ctxt =
+  let val elem = raw_elem |> map_ctxt
    {binding = tap Name.of_binding,
     typ = I,
     term = I,
     pattern = I,
     fact = ProofContext.get_fact ctxt,
-    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)};
-
-in
-
-fun activate x = gen_activate prep_facts x;
-fun activate_i x = gen_activate (K I) x;
+    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
+  in activate_i elem ctxt end;
 
 end;
-
-end;
diff -r fcd49e932503 -r 9960ff945c52 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:47:58 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Mar 29 18:06:14 2009 +0200
@@ -416,7 +416,7 @@
        prep true false ([], []) I raw_elems raw_concl context;
      val (_, context') = context |>
        ProofContext.set_stmt true |>
-       activate elems;
+       fold_map activate elems;
   in (concl, context') end;
 
 in
@@ -444,7 +444,7 @@
       fold (Context.proof_map o Locale.activate_facts) deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
-      activate elems;
+      fold_map activate elems;
   in ((fixed, deps, elems'), (parms, ctxt')) end;
 
 in
diff -r fcd49e932503 -r 9960ff945c52 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Mar 29 17:47:58 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Mar 29 18:06:14 2009 +0200
@@ -370,7 +370,7 @@
 
 fun add_thmss loc kind args ctxt =
   let
-    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
     val ctxt'' = ctxt' |> ProofContext.theory (
       (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
         #>