src/Pure/Isar/proof_context.ML
changeset 44419 f231a7594e54
parent 43630 0bbb56867091
child 44423 156c822f181a
     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