# HG changeset patch
# User wenzelm
# Date 1717766401 -7200
# Node ID eec06d39e5fab2d41b0ecca3773be010d3582f63
# Parent  453eccb886f2a00b7c66c13abd8c24fc3a0fd576
clarified signature: prefer explicit operation;

diff -r 453eccb886f2 -r eec06d39e5fa src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Jun 07 15:01:16 2024 +0200
+++ b/src/Pure/logic.ML	Fri Jun 07 15:20:01 2024 +0200
@@ -48,6 +48,7 @@
   val const_of_class: class -> string
   val class_of_const: string -> class
   val mk_of_class: typ * class -> term
+  val match_of_class: term -> typ * string  (*exception Match*)
   val dest_of_class: term -> typ * class
   val mk_of_sort: typ * sort -> term list
   val name_classrel: string * string -> string
@@ -303,6 +304,9 @@
 fun mk_of_class (ty, c) =
   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
 
+fun match_of_class (Const (c, _) $ Const ("Pure.type", Type ("itself", [ty]))) =
+  if String.isSuffix class_suffix c then (ty, class_of_const c) else raise Match;
+
 fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   | dest_of_class t = raise TERM ("dest_of_class", [t]);
 
diff -r 453eccb886f2 -r eec06d39e5fa src/Pure/zterm.ML
--- a/src/Pure/zterm.ML	Fri Jun 07 15:01:16 2024 +0200
+++ b/src/Pure/zterm.ML	Fri Jun 07 15:20:01 2024 +0200
@@ -604,11 +604,10 @@
           | [T] => ZConst1 (c, ztyp T)
           | Ts => ZConst (c, map ztyp Ts))
       | zterm (Abs (a, T, b)) = ZAbs (a, ztyp T, zterm b)
-      | zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) =
-          if String.isSuffix Logic.class_suffix c then
-            OFCLASS (ztyp (Logic.dest_type u), Logic.class_of_const c)
-          else ZApp (zterm t, zterm u)
-      | zterm (t $ u) = ZApp (zterm t, zterm u);
+      | zterm (tm as t $ u) =
+          (case try Logic.match_of_class tm of
+            SOME (T, c) => OFCLASS (ztyp T, c)
+          | NONE => ZApp (zterm t, zterm u));
   in {ztyp = ztyp, zterm = zterm} end;
 
 val zterm_of = #zterm o zterm_cache;