# 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),