1.1 --- a/src/Pure/Isar/proof_context.ML Sat Jun 25 17:17:49 2011 +0200
1.2 +++ b/src/Pure/Isar/proof_context.ML Sat Jun 25 18:15:36 2011 +0200
1.3 @@ -362,7 +362,6 @@
1.4 val (syms, pos) = Syntax.read_token text;
1.5 val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
1.6 handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
1.7 - val _ = Context_Position.report ctxt pos (Markup.tclass c);
1.8 val _ = Context_Position.report ctxt pos (Name_Space.markup (Type.class_space tsig) c);
1.9 in c end;
1.10