1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 02 21:02:27 2014 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 02 21:13:29 2014 +0100
     1.3 @@ -441,26 +441,7 @@
     1.4    in (xs ~~ Ts, ctxt') end;
     1.5  
     1.6  
     1.7 -(* type and constant names *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun prep_const_proper ctxt strict (c, pos) =
    1.12 -  let
    1.13 -    fun err msg = error (msg ^ Position.here pos);
    1.14 -    val consts = consts_of ctxt;
    1.15 -    val t as Const (d, _) =
    1.16 -      (case Variable.lookup_const ctxt c of
    1.17 -        SOME d =>
    1.18 -          Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
    1.19 -      | NONE => Consts.read_const consts (c, pos));
    1.20 -    val _ =
    1.21 -      if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
    1.22 -      else ();
    1.23 -    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
    1.24 -  in t end;
    1.25 -
    1.26 -in
    1.27 +(* type names *)
    1.28  
    1.29  fun read_type_name ctxt strict text =
    1.30    let
    1.31 @@ -488,6 +469,27 @@
    1.32    | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
    1.33  
    1.34  
    1.35 +(* constant names *)
    1.36 +
    1.37 +local
    1.38 +
    1.39 +fun prep_const_proper ctxt strict (c, pos) =
    1.40 +  let
    1.41 +    fun err msg = error (msg ^ Position.here pos);
    1.42 +    val consts = consts_of ctxt;
    1.43 +    val t as Const (d, _) =
    1.44 +      (case Variable.lookup_const ctxt c of
    1.45 +        SOME d =>
    1.46 +          Const (d, Consts.type_scheme (consts_of ctxt) d handle TYPE (msg, _, _) => err msg)
    1.47 +      | NONE => Consts.read_const consts (c, pos));
    1.48 +    val _ =
    1.49 +      if strict then ignore (Consts.the_const consts d) handle TYPE (msg, _, _) => err msg
    1.50 +      else ();
    1.51 +    val _ = Context_Position.report ctxt pos (Name_Space.markup (Consts.space_of consts) d);
    1.52 +  in t end;
    1.53 +
    1.54 +in
    1.55 +
    1.56  fun read_const_proper ctxt strict =
    1.57    prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
    1.58