# HG changeset patch
# User wenzelm
# Date 1407244031 -7200
# Node ID 0c104888f1caa7510c939b1833383ae31523810d
# Parent  8f074e6e22fc7da4fabca74f10ae2f045aab9599
avoid duplication of warnings stemming from simp/intro declarations etc.;

diff -r 8f074e6e22fc -r 0c104888f1ca src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 05 12:56:15 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 05 15:07:11 2014 +0200
@@ -347,10 +347,11 @@
   let val table = get_methods ctxt
   in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
-fun method_closure ctxt src0 =
+fun method_closure ctxt0 src0 =
   let
-    val (src1, meth) = check_src ctxt src0;
+    val (src1, meth) = check_src ctxt0 src0;
     val src2 = Args.init_assignable src1;
+    val ctxt = Context_Position.not_really ctxt0;
     val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
   in Args.closure src2 end;