src/Pure/Isar/expression.ML

   let
      val ((_, _, elems, concl), _) =
        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
 
 fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;

     val context' = context |>
       fix_params fixed |>
       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
 
 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;