clarified context;
tuned;

--- a/src/Pure/Isar/expression.ML	Sun Jun 14 19:15:31 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Jun 14 20:10:21 2015 +0200
@@ -281,9 +281,9 @@
       (fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
     val (elem_css', [concl_cs']) = chop (length elem_css) css';
   in
-    (map restore_inst (insts ~~ inst_cs'),
+    ((map restore_inst (insts ~~ inst_cs'),
       map restore_elem (elems ~~ elem_css'),
-      concl_cs', ctxt')
+      concl_cs'), ctxt')
   end;
 
 end;
@@ -374,7 +374,7 @@
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
-        val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
+        val ((insts'', _, _), _) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
         val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
@@ -389,15 +389,13 @@
         val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem;
       in (elems', ctxt') end;
 
-    fun prep_concl raw_concl (insts, elems, ctxt) =
-      let
-        val concl = parse_concl parse_prop ctxt raw_concl;
-      in check_autofix insts elems concl ctxt end;
-
     val fors = fold_map prep_var_inst fixed ctxt1 |> fst;
     val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
 
+    fun prep_concl elems ctxt =
+      check_autofix insts' elems (parse_concl parse_prop ctxt raw_concl) ctxt;
+
     val _ =
       if fixed_frees then ()
       else
@@ -406,23 +404,24 @@
         | frees => error ("Illegal free variables in expression: " ^
             commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
 
-    val ctxt4 = init_body ctxt3;
-    val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
-    val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
+    val ((insts, elems', concl), ctxt4) = ctxt3
+      |> init_body
+      |> fold_map prep_elem raw_elems
+      |-> prep_concl;
 
 
     (* parameters from expression and elements *)
 
     val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
       (Fixes fors :: elems');
-    val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
+    val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4;
 
     val fors' = finish_fixes parms fors;
     val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
-    val deps = map (finish_inst ctxt6) insts;
-    val elems'' = map (finish_elem (ctxt1, ctxt6) parms do_close) elems';
+    val deps = map (finish_inst ctxt5) insts;
+    val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
 
-  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end;
+  in ((fixed, deps, elems'', concl), (parms, ctxt5)) end;
 
 in