# HG changeset patch
# User blanchet
# Date 1300369431 -3600
# Node ID ea02b9ee30854b73c27ef8dc3c066d5009bc676c
# Parent  7f2793d51efcd709b4b6e753ed55d2da95f8f08e
prevent an exception if "card" is empty (e.g., "nitpick [card]")

diff -r 7f2793d51efc -r ea02b9ee3085 src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Mar 17 11:18:31 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Mar 17 14:43:51 2011 +0100
@@ -216,7 +216,8 @@
 
 fun rank_of_row (_, ks) = length ks
 fun rank_of_block block = fold Integer.max (map rank_of_row block) 1
-fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
+fun project_row _ (y, []) = (y, [1]) (* desperate measure *)
+  | project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))])
 fun project_block (column, block) = map (project_row column) block
 
 fun lookup_ints_assign eq assigns key =
@@ -353,13 +354,14 @@
   let
     val (card_assigns, max_assigns) =
       maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
-    val card_assigns =
-      repair_card_assigns hol_ctxt binarize (card_assigns, max_assigns) |> the
   in
-    SOME (map (repair_iterator_assign ctxt card_assigns) card_assigns,
-          max_assigns)
+    (card_assigns, max_assigns)
+    |> repair_card_assigns hol_ctxt binarize
+    |> Option.map
+           (fn card_assigns =>
+               (map (repair_iterator_assign ctxt card_assigns) card_assigns,
+                max_assigns))
   end
-  handle Option.Option => NONE
 
 fun offset_table_for_card_assigns dtypes assigns =
   let