src/Pure/sign.ML
changeset 35395 ba804f4c82c6
parent 35359 3ec03a3cd9d0
child 35412 b8dead547d9e
     1.1 --- a/src/Pure/sign.ML	Sat Feb 27 13:32:05 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Feb 27 13:32:18 2010 +0100
     1.3 @@ -404,8 +404,13 @@
     1.4  
     1.5  (* classes *)
     1.6  
     1.7 -fun read_class thy c = certify_class thy (intern_class thy c)
     1.8 -  handle TYPE (msg, _, _) => error msg;
     1.9 +fun read_class thy text =
    1.10 +  let
    1.11 +    val (syms, pos) = Syntax.read_token text;
    1.12 +    val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
    1.13 +      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
    1.14 +    val _ = Position.report (Markup.tclass c) pos;
    1.15 +  in c end;
    1.16  
    1.17  
    1.18  (* type arities *)