1.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4          val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
     1.5        in (i + 1, insts', ctxt'') end;
     1.6  
     1.7 -    fun prep_elem insts raw_elem ctxt =
     1.8 +    fun prep_elem raw_elem ctxt =
     1.9        let
    1.10          val ctxt' = ctxt
    1.11            |> Context_Position.set_visible false
    1.12 @@ -391,7 +391,7 @@
    1.13              commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
    1.14  
    1.15      val ctxt4 = init_body ctxt3;
    1.16 -    val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4;
    1.17 +    val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
    1.18      val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
    1.19  
    1.20      (* Retrieve parameter types *)