"_type_prop" is syntax const -- recovered printing of OFCLASS;

--- a/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:33:33 2010 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Wed Mar 03 00:50:47 2010 +0100
@@ -266,7 +266,7 @@
    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
-  []
+  ["_type_prop"]
   (map SynExt.mk_trfun
    [("_class_name", class_name_tr o read_class o ProofContext.theory_of),
     ("_classes", classes_tr o read_class o ProofContext.theory_of),