--- a/src/Pure/Isar/proof_context.ML Sun Mar 02 21:02:27 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 02 21:13:29 2014 +0100
@@ -441,26 +441,7 @@
in (xs ~~ Ts, ctxt') end;
-(* type and constant names *)
-
-local
-
-fun prep_const_proper ctxt strict (c, pos) =
- let
- fun err msg = error (msg ^ Position.here pos);
- val consts = consts_of ctxt;
- val t as Const (d, _) =
- (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_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
+(* type names *)
fun read_type_name ctxt strict text =
let
@@ -488,6 +469,27 @@
| T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
+(* constant names *)
+
+local
+
+fun prep_const_proper ctxt strict (c, pos) =
+ let
+ fun err msg = error (msg ^ Position.here pos);
+ val consts = consts_of ctxt;
+ val t as Const (d, _) =
+ (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_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
+
fun read_const_proper ctxt strict =
prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;