# HG changeset patch
# User wenzelm
# Date 1693321212 -7200
# Node ID 9ccd5e8737cbd9bc721a7a39a654f8d8e2090dcb
# Parent  2401b5d9cee91230e87f779d1fd26afad3a7ba5c
clarified signature: prefer enum types;

diff -r 2401b5d9cee9 -r 9ccd5e8737cb src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 29 16:55:49 2023 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 29 17:00:12 2023 +0200
@@ -239,14 +239,12 @@
 
   /* approximative syntax */
 
-  object Assoc extends Enumeration {
-    val NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC = Value
-  }
+  enum Assoc { case NO_ASSOC, LEFT_ASSOC, RIGHT_ASSOC }
 
   sealed abstract class Syntax
   case object No_Syntax extends Syntax
   case class Prefix(delim: String) extends Syntax
-  case class Infix(assoc: Assoc.Value, delim: String, pri: Int) extends Syntax
+  case class Infix(assoc: Assoc, delim: String, pri: Int) extends Syntax
 
   def decode_syntax: XML.Decode.T[Syntax] =
     XML.Decode.variant(List(
@@ -255,7 +253,7 @@
       { case (Nil, body) =>
           import XML.Decode._
           val (ass, delim, pri) = triple(int, string, int)(body)
-          Infix(Assoc(ass), delim, pri) }))
+          Infix(Assoc.fromOrdinal(ass), delim, pri) }))
 
 
   /* types */