tuned;

--- a/src/Pure/Isar/expression.ML	Thu May 12 10:03:17 2016 +0200
+++ b/src/Pure/Isar/expression.ML	Thu May 12 10:16:52 2016 +0200
@@ -250,18 +250,19 @@
       (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines
   | restore_elem (Notes notes, _) = Notes notes;
 
-fun check cs context =
+fun prep (_, pats) (ctxt, t :: ts) =
+  let val ctxt' = Variable.auto_fixes t ctxt
+  in
+    ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
+      (ctxt', ts))
+  end;
+
+fun check cs ctxt =
   let
-    fun prep (_, pats) (ctxt, t :: ts) =
-      let val ctxt' = Variable.auto_fixes t ctxt
-      in
-        ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats),
-          (ctxt', ts))
-      end;
-    val (cs', (context', _)) = fold_map prep cs
-      (context, Syntax.check_terms
-        (Proof_Context.set_mode Proof_Context.mode_schematic context) (map fst cs));
-  in (cs', context') end;
+    val (cs', (ctxt', _)) = fold_map prep cs
+      (ctxt, Syntax.check_terms
+        (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs));
+  in (cs', ctxt') end;
 
 in
 
@@ -438,15 +439,15 @@
 
 local
 
-fun prep_statement prep activate raw_elems raw_stmt context =
+fun prep_statement prep activate raw_elems raw_stmt ctxt =
   let
     val ((_, _, elems, concl), _) =
       prep {strict = true, do_close = false, fixed_frees = true}
-        ([], []) I raw_elems raw_stmt context;
-    val (_, context') = context
+        ([], []) I raw_elems raw_stmt ctxt;
+    val (_, ctxt') = ctxt
       |> Proof_Context.set_stmt true
       |> fold_map activate elems;
-  in (concl, context') end;
+  in (concl, ctxt') end;
 
 in
 
@@ -498,21 +499,21 @@
     |> map (Morphism.term morph)
   end;
 
-fun prep_goal_expression prep expression context =
+fun prep_goal_expression prep expression ctxt =
   let
-    val thy = Proof_Context.theory_of context;
+    val thy = Proof_Context.theory_of ctxt;
 
     val ((fixed, deps, _, _), _) =
       prep {strict = true, do_close = true, fixed_frees = true} expression I []
-        (Element.Shows []) context;
+        (Element.Shows []) ctxt;
     (* proof obligations *)
     val propss = map (props_of thy) deps;
 
-    val goal_ctxt = context |>
-      fix_params fixed |>
-      (fold o fold) Variable.auto_fixes propss;
+    val goal_ctxt = ctxt
+      |> fix_params fixed
+      |> (fold o fold) Variable.auto_fixes propss;
 
-    val export = Variable.export_morphism goal_ctxt context;
+    val export = Variable.export_morphism goal_ctxt ctxt;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     val exp_typ = Logic.type_map exp_term;