# HG changeset patch
# User wenzelm
# Date 1463041319 -7200
# Node ID 88474b9fc8440dd3994dd1a4a8da387ce4067749
# Parent  0054992a86b72def8c97cde27777a12e7856fb4e
tuned;

diff -r 0054992a86b7 -r 88474b9fc844 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu May 12 10:16:52 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 12 10:21:59 2016 +0200
@@ -464,19 +464,19 @@
 
 local
 
-fun prep_declaration prep activate raw_import init_body raw_elems context =
+fun prep_declaration prep activate raw_import init_body raw_elems ctxt =
   let
-    val ((fixed, deps, elems, _), (parms, ctxt')) =
+    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