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 ();