diff -r 0f6e8c4144a5 -r 106bd5a4af22 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
@@ -364,7 +364,7 @@
         val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
       in (i + 1, insts', ctxt'') end;
 
-    fun prep_elem insts raw_elem ctxt =
+    fun prep_elem raw_elem ctxt =
       let
         val ctxt' = ctxt
           |> Context_Position.set_visible false
@@ -391,7 +391,7 @@
             commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
 
     val ctxt4 = init_body ctxt3;
-    val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4;
+    val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
     val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)