src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Fri Mar 09 17:24:42 2012 +0000
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 09 20:04:19 2012 +0100
@@ -839,7 +839,7 @@
 
 fun retrieve_thms pick ctxt (Facts.Fact s) =
       let
-        val (_, pos) = Syntax.read_token s;
+        val pos = Syntax.read_token_pos s;
         val prop =
           Syntax.read_prop (ctxt |> set_mode mode_default |> allow_dummies) s
           |> singleton (Variable.polymorphic ctxt);