1.1 --- a/src/Pure/Isar/method.ML	Tue Aug 05 12:56:15 2014 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Aug 05 15:07:11 2014 +0200
     1.3 @@ -347,10 +347,11 @@
     1.4    let val table = get_methods ctxt
     1.5    in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
     1.6  
     1.7 -fun method_closure ctxt src0 =
     1.8 +fun method_closure ctxt0 src0 =
     1.9    let
    1.10 -    val (src1, meth) = check_src ctxt src0;
    1.11 +    val (src1, meth) = check_src ctxt0 src0;
    1.12      val src2 = Args.init_assignable src1;
    1.13 +    val ctxt = Context_Position.not_really ctxt0;
    1.14      val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
    1.15    in Args.closure src2 end;
    1.16