# HG changeset patch
# User haftmann
# Date 1525630825 0
# Node ID e2bb1d95cbd06bd4eaf9959fdc1f7ef6a8bdb5fd
# Parent  5f3cffe163119a3342f065493567a6446ef23e5f
more appropriate notion of emptiness

diff -r 5f3cffe16311 -r e2bb1d95cbd0 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun May 06 23:59:14 2018 +0100
+++ b/src/Pure/Isar/class.ML	Sun May 06 18:20:25 2018 +0000
@@ -196,13 +196,13 @@
         ([Pretty.keyword1 "class", Pretty.brk 1,
           Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
           Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
-          (case try (Axclass.get_info thy) class of
-            NONE => []
-          | SOME {params, ...} =>
+          (case (these o Option.map #params o try (Axclass.get_info thy)) class of
+            [] => []
+          | params =>
               [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
-          (case Symtab.lookup arities class of
-            NONE => []
-          | SOME ars =>
+          (case (these o Symtab.lookup arities) class of
+            [] => []
+          | ars =>
               [Pretty.fbrk, Pretty.big_list "instances:"
                 (map (prt_arity class) (sort (Name_Space.extern_ord ctxt type_space) ars))]));
   in