src/Pure/Syntax/type_ext.ML

    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
    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),
     ("_type_name", type_name_tr o read_type o ProofContext.theory_of),
     ("_tapp", tapp_ast_tr o read_type o ProofContext.theory_of),