src/Pure/type.ML
changeset 79470 9fcf73580c62
parent 79469 deb50d396ff7
--- a/src/Pure/type.ML	Wed Jan 10 13:37:29 2024 +0100
+++ b/src/Pure/type.ML	Wed Jan 10 13:43:10 2024 +0100
@@ -18,6 +18,8 @@
     Logical_Type of int |
     Abbreviation of string list * typ * bool |
     Nonterminal
+  val decl_args: decl -> int
+  val decl_logical: decl -> bool
   type tsig
   val eq_tsig: tsig * tsig -> bool
   val rep_tsig: tsig ->
@@ -161,6 +163,9 @@
   | decl_args (Abbreviation (vs, _, _)) = length vs
   | decl_args Nonterminal = 0;
 
+fun decl_logical (Logical_Type _) = true
+  | decl_logical _ = false;
+
 
 (* type tsig *)