# HG changeset patch
# User haftmann
# Date 1191519714 -7200
# Node ID 01b14b37eca3fe739e2a6e2fa06b3020d141d2ce
# Parent  199c48ec5a09f5d5d023ee7bb31d4602f71a34d9
clarified name suffix

diff -r 199c48ec5a09 -r 01b14b37eca3 src/Tools/code/code_name.ML
--- a/src/Tools/code/code_name.ML	Thu Oct 04 19:41:53 2007 +0200
+++ b/src/Tools/code/code_name.ML	Thu Oct 04 19:41:54 2007 +0200
@@ -100,7 +100,7 @@
 (* identifier categories *)
 
 val suffix_class = "class";
-val suffix_classrel = "clsrel"
+val suffix_classrel = "classrel"
 val suffix_tyco = "tyco";
 val suffix_instance = "inst";
 val suffix_const = "const";