src/Pure/Isar/expression.ML

       prep false true context raw_import raw_elems [];
     (* Declare parameters and imported facts *)
     val context' = context |>
       ProofContext.add_fixes_i fixed |> snd |>
       fold NewLocale.activate_local_facts deps;
-    val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
+    val (elems', _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
 
 in
 
 fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;