diff -r f33b036ef318 -r 768d14a67256 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:44:29 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 15 19:45:05 2009 +0100
@@ -883,8 +883,7 @@
           |> singleton (Variable.polymorphic ctxt);
 
         fun prove_fact th =
-          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])))
-          |> Thm.default_position_of th;
+          Goal.prove ctxt [] [] prop (K (ALLGOALS (fact_tac [th])));
         val res =
           (case get_first (try prove_fact) (potential_facts ctxt prop) of
             SOME res => res
@@ -934,12 +933,12 @@
     val name = full_name ctxt b;
     val _ = Context_Position.report_visible ctxt (Markup.local_fact_decl name) pos;
 
-    val facts = PureThy.name_thmss false pos name raw_facts;
+    val facts = PureThy.name_thmss false name raw_facts;
     fun app (th, attrs) x =
       swap (Library.foldl_map
         (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;
-    val thms = PureThy.name_thms false false pos name (flat res);
+    val thms = PureThy.name_thms false false name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
   in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);