# HG changeset patch
# User wenzelm
# Date 1704890590 -3600
# Node ID 9fcf73580c6299050ec897bf9a44a6415511eb02
# Parent  deb50d396ff798e74431e35dd5d11594c3c489b1
clarified signature;

diff -r deb50d396ff7 -r 9fcf73580c62 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:37:29 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:43:10 2024 +0100
@@ -533,13 +533,10 @@
   else
     let
       val ((d, reports), decl) = Type.check_decl (Context.Proof ctxt) (tsig_of ctxt) (c, pos);
-      fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
-      val args =
-        (case decl of
-          Type.Logical_Type n => n
-        | Type.Abbreviation (vs, _, _) => if strict then err () else length vs
-        | Type.Nonterminal => if strict then err () else 0);
-    in (Type (d, replicate args dummyT), reports) end;
+      val _ =
+        if strict andalso not (Type.decl_logical decl)
+        then error ("Bad type name: " ^ quote d ^ Position.here pos) else ();
+    in (Type (d, replicate (Type.decl_args decl) dummyT), reports) end;
 
 fun read_type_name flags ctxt text =
   let
diff -r deb50d396ff7 -r 9fcf73580c62 src/Pure/type.ML
--- 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 *)