# HG changeset patch
# User wenzelm
# Date 1703968848 -3600
# Node ID 40e3d97b277ed4d0ab1a6580cea18683bfdebba0
# Parent  2ff5ffd8731b2bb72f3c3e526f1f17593ff7fa6b
tuned whitespace;

diff -r 2ff5ffd8731b -r 40e3d97b277e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/sign.ML	Sat Dec 30 21:40:48 2023 +0100
@@ -23,7 +23,8 @@
   val subsort: theory -> sort * sort -> bool
   val of_sort: theory -> typ * sort -> bool
   val inter_sort: theory -> sort * sort -> sort
-  val witness_sorts: theory -> (typ * sort) list -> sort Ord_List.T ->
+  val witness_sorts: theory ->
+    (typ * sort) list -> sort Ord_List.T ->
     (typ * sort) list * sort Ord_List.T
   val logical_types: theory -> string list
   val typ_instance: theory -> typ * typ -> bool
diff -r 2ff5ffd8731b -r 40e3d97b277e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/sorts.ML	Sat Dec 30 21:40:48 2023 +0100
@@ -64,7 +64,8 @@
     typ * sort -> 'a list   (*exception CLASS_ERROR*)
   val classrel_derivation: algebra ->
     ('a * class -> class -> 'a) -> 'a * class -> class -> 'a  (*exception CLASS_ERROR*)
-  val witness_sorts: algebra -> string list -> (typ * sort) list -> sort Ord_List.T ->
+  val witness_sorts: algebra -> string list ->
+    (typ * sort) list -> sort Ord_List.T ->
     (typ * sort) list * sort Ord_List.T
 end;
 
diff -r 2ff5ffd8731b -r 40e3d97b277e src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Dec 30 21:35:00 2023 +0100
+++ b/src/Pure/type.ML	Sat Dec 30 21:40:48 2023 +0100
@@ -38,7 +38,8 @@
   val cert_class: tsig -> class -> class
   val cert_sort: tsig -> sort -> sort
   val minimize_sort: tsig -> sort -> sort
-  val witness_sorts: tsig -> (typ * sort) list -> sort Ord_List.T ->
+  val witness_sorts: tsig ->
+    (typ * sort) list -> sort Ord_List.T ->
     (typ * sort) list * sort Ord_List.T
   type mode
   val mode_default: mode