# HG changeset patch
# User wenzelm
# Date 1267573847 -3600
# Node ID 73cc288b4f83ae3492ce04968689545d5333e4c4
# Parent  b8863ee98f568e90a02886bdf1da624fad356770
"_type_prop" is syntax const -- recovered printing of OFCLASS;

diff -r b8863ee98f56 -r 73cc288b4f83 src/Pure/Syntax/type_ext.ML
--- 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),