src/Pure/Isar/proof_context.ML

       (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, pos));
     val _ =
-      if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
+      if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
       else ();
     val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
   in t end;
 
 in