src/Pure/Isar/proof_context.ML
changeset 42469 daa93275880e
parent 42468 aea61c5f88c3
child 42488 4638622bcaa1
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:25:50 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 23 18:46:01 2011 +0200
@@ -462,7 +462,7 @@
       (case Variable.lookup_const ctxt c of
         SOME d =>
           Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
-      | NONE => Consts.read_const consts c);
+      | NONE => Consts.read_const consts (c, pos));
     val _ =
       if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
       else ();