# HG changeset patch
# User wenzelm
# Date 1704890249 -3600
# Node ID deb50d396ff798e74431e35dd5d11594c3c489b1
# Parent  953ada87ea37701952f1992beccc00c99174d7b0
tuned signature;

diff -r 953ada87ea37 -r deb50d396ff7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -536,7 +536,7 @@
       fun err () = error ("Bad type name: " ^ quote d ^ Position.here pos);
       val args =
         (case decl of
-          Type.LogicalType n => n
+          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;
diff -r 953ada87ea37 -r deb50d396ff7 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -94,7 +94,7 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, Type.LogicalType n) =
+    fun pretty_type syn (t, Type.Logical_Type n) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
       | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
diff -r 953ada87ea37 -r deb50d396ff7 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -127,7 +127,7 @@
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close>
-    (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
+    (type_name "logical type" (fn (c, Type.Logical_Type _) => c)) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close>
     (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
   ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close>
diff -r 953ada87ea37 -r deb50d396ff7 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/Thy/export_theory.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -219,7 +219,7 @@
     val _ =
       export_entities "types" Sign.type_space (Name_Space.dest_table (#types rep_tsig))
         (fn c =>
-          (fn Type.LogicalType n =>
+          (fn Type.Logical_Type n =>
                 SOME (fn () =>
                   encode_type (get_syntax_type thy_ctxt c, Name.invent Name.context Name.aT n, NONE))
             | Type.Abbreviation (args, U, false) =>
diff -r 953ada87ea37 -r deb50d396ff7 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Jan 10 13:33:36 2024 +0100
+++ b/src/Pure/type.ML	Wed Jan 10 13:37:29 2024 +0100
@@ -15,7 +15,7 @@
   val appl_error: Proof.context -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
   datatype decl =
-    LogicalType of int |
+    Logical_Type of int |
     Abbreviation of string list * typ * bool |
     Nonterminal
   type tsig
@@ -153,11 +153,11 @@
 (* type declarations *)
 
 datatype decl =
-  LogicalType of int |
+  Logical_Type of int |
   Abbreviation of string list * typ * bool |
   Nonterminal;
 
-fun decl_args (LogicalType n) = n
+fun decl_args (Logical_Type n) = n
   | decl_args (Abbreviation (vs, _, _)) = length vs
   | decl_args Nonterminal = 0;
 
@@ -192,7 +192,7 @@
 fun build_tsig (classes, default, types) =
   let
     val log_types =
-      Name_Space.fold_table (fn (c, LogicalType n) => cons (c, n) | _ => I) types []
+      Name_Space.fold_table (fn (c, Logical_Type n) => cons (c, n) | _ => I) types []
       |> Library.sort (int_ord o apply2 snd) |> map fst;
   in make_tsig (classes, default, types, log_types) end;
 
@@ -280,7 +280,7 @@
             if length args <> decl_args decl then err T (bad_nargs c)
             else
               (case decl of
-                LogicalType _ => Type (c, Same.map typ args)
+                Logical_Type _ => Type (c, Same.map typ args)
               | Abbreviation (vs, U, syntactic) =>
                   if syntactic andalso logical then err_syntactic T c
                   else if normalize then inst_typ vs args U
@@ -304,7 +304,7 @@
 
 fun arity_number tsig a =
   (case lookup_type tsig a of
-    SOME (LogicalType n) => n
+    SOME (Logical_Type n) => n
   | _ => error (undecl_type a));
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
@@ -629,7 +629,7 @@
   let
     val _ =
       (case lookup_type tsig t of
-        SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
+        SOME (Logical_Type n) => if length Ss <> n then error (bad_nargs t) else ()
       | SOME _ => error ("Logical type constructor expected: " ^ quote t)
       | NONE => error (undecl_type t));
     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
@@ -680,7 +680,7 @@
 
 fun add_type context (c, n) =
   if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
-  else map_types (new_decl context (c, LogicalType n));
+  else map_types (new_decl context (c, Logical_Type n));
 
 fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let