simplified Element.activate(_i): singleton version;
authorwenzelm
Sun Mar 29 18:06:14 2009 +0200 (2009-03-29)
changeset 307779960ff945c52
parent 30776 fcd49e932503
child 30778 46de352e018b
simplified Element.activate(_i): singleton version;
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/element.ML	Sun Mar 29 17:47:58 2009 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 29 18:06:14 2009 +0200
     1.3 @@ -61,8 +61,8 @@
     1.4    val eq_morphism: theory -> thm list -> morphism
     1.5    val transfer_morphism: theory -> morphism
     1.6    val init: context_i -> Context.generic -> Context.generic
     1.7 -  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
     1.8 -  val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
     1.9 +  val activate_i: context_i -> Proof.context -> context_i * Proof.context
    1.10 +  val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
    1.11  end;
    1.12  
    1.13  structure Element: ELEMENT =
    1.14 @@ -516,30 +516,20 @@
    1.15  
    1.16  (* activate *)
    1.17  
    1.18 -local
    1.19 -
    1.20 -fun gen_activate prep_facts raw_elems ctxt =
    1.21 +fun activate_i elem ctxt =
    1.22    let
    1.23 -    fun activate elem ctxt' =
    1.24 -      let val elem' = map_ctxt_attrib Args.assignable (prep_facts ctxt' elem)
    1.25 -      in (elem', Context.proof_map (init elem') ctxt') end;
    1.26 -    val (elems, ctxt') = fold_map activate raw_elems ctxt;
    1.27 -  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
    1.28 +    val elem' = map_ctxt_attrib Args.assignable elem;
    1.29 +    val ctxt' = Context.proof_map (init elem') ctxt;
    1.30 +  in (map_ctxt_attrib Args.closure elem', ctxt') end;
    1.31  
    1.32 -fun prep_facts ctxt =
    1.33 -  map_ctxt
    1.34 +fun activate raw_elem ctxt =
    1.35 +  let val elem = raw_elem |> map_ctxt
    1.36     {binding = tap Name.of_binding,
    1.37      typ = I,
    1.38      term = I,
    1.39      pattern = I,
    1.40      fact = ProofContext.get_fact ctxt,
    1.41 -    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)};
    1.42 -
    1.43 -in
    1.44 -
    1.45 -fun activate x = gen_activate prep_facts x;
    1.46 -fun activate_i x = gen_activate (K I) x;
    1.47 +    attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
    1.48 +  in activate_i elem ctxt end;
    1.49  
    1.50  end;
    1.51 -
    1.52 -end;
     2.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 17:47:58 2009 +0200
     2.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 18:06:14 2009 +0200
     2.3 @@ -416,7 +416,7 @@
     2.4         prep true false ([], []) I raw_elems raw_concl context;
     2.5       val (_, context') = context |>
     2.6         ProofContext.set_stmt true |>
     2.7 -       activate elems;
     2.8 +       fold_map activate elems;
     2.9    in (concl, context') end;
    2.10  
    2.11  in
    2.12 @@ -444,7 +444,7 @@
    2.13        fold (Context.proof_map o Locale.activate_facts) deps;
    2.14      val (elems', _) = context' |>
    2.15        ProofContext.set_stmt true |>
    2.16 -      activate elems;
    2.17 +      fold_map activate elems;
    2.18    in ((fixed, deps, elems'), (parms, ctxt')) end;
    2.19  
    2.20  in
     3.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 29 17:47:58 2009 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 29 18:06:14 2009 +0200
     3.3 @@ -370,7 +370,7 @@
     3.4  
     3.5  fun add_thmss loc kind args ctxt =
     3.6    let
     3.7 -    val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
     3.8 +    val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
     3.9      val ctxt'' = ctxt' |> ProofContext.theory (
    3.10        (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
    3.11          #>