# HG changeset patch
# User wenzelm
# Date 1672086500 -3600
# Node ID 9e5a27486ca23defab1a0d112cedc2d30dec078c
# Parent  de9efab17e4724642798861efeed6168d30bd2c3
tuned signature;

diff -r de9efab17e47 -r 9e5a27486ca2 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Mon Dec 26 19:13:37 2022 +0100
+++ b/src/Pure/logic.ML	Mon Dec 26 21:28:20 2022 +0100
@@ -44,6 +44,7 @@
   val mk_type: typ -> term
   val dest_type: term -> typ
   val type_map: (term -> term) -> typ -> typ
+  val class_suffix: string
   val const_of_class: class -> string
   val class_of_const: string -> class
   val mk_of_class: typ * class -> term
@@ -288,11 +289,11 @@
 
 (* const names *)
 
-val classN = "_class";
+val class_suffix = "_class";
 
-val const_of_class = suffix classN;
+val const_of_class = suffix class_suffix;
 
-fun class_of_const c = unsuffix classN c
+fun class_of_const c = unsuffix class_suffix c
   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);