src/Pure/Isar/expression.ML

 fun fix_params params =
   Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
 
 local
 
-fun prep_declaration prep activate raw_import init_body raw_elems context =
-  let
-    val ((fixed, deps, elems, _), (parms, ctxt')) =
+fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
+  let
+    val ((fixed, deps, elems, _), (parms, ctxt0)) =
       prep {strict = false, do_close = true, fixed_frees = false}
-        raw_import init_body raw_elems (Element.Shows []) context;
+        raw_import init_body raw_elems (Element.Shows []) ctxt;
     (* Declare parameters and imported facts *)
-    val context' = context |>
-      fix_params fixed |>
-      fold (Context.proof_map o Locale.activate_facts NONE) deps;
-    val (elems', context'') = context' |>
-      Proof_Context.set_stmt true |>
-      fold_map activate elems;
-  in ((fixed, deps, elems', context''), (parms, ctxt')) end;
+    val ctxt' = ctxt
+      |> fix_params fixed
+      |> fold (Context.proof_map o Locale.activate_facts NONE) deps;
+    val (elems', ctxt'') = ctxt'
+      |> Proof_Context.set_stmt true
+      |> fold_map activate elems;
+  in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end;
 
 in
 
 fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
 fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x;