# HG changeset patch
# User traytel
# Date 1409642903 -7200
# Node ID 0774d32fe74f4623b17f6e23ad7d3538984269b2
# Parent  b563ec62d04e18ae5d1d2959ddb86bfd6de711eb
silenced nonexhaustive primrec warnings

diff -r b563ec62d04e -r 0774d32fe74f src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 02 08:24:42 2014 +0200
+++ b/src/HOL/List.thy	Tue Sep 02 09:28:23 2014 +0200
@@ -52,7 +52,7 @@
 
 subsection {* Basic list processing functions *}
 
-primrec last :: "'a list \<Rightarrow> 'a" where
+primrec (nonexhaustive) last :: "'a list \<Rightarrow> 'a" where
 "last (x # xs) = (if xs = [] then x else last xs)"
 
 primrec butlast :: "'a list \<Rightarrow> 'a list" where
@@ -117,7 +117,7 @@
   -- {*Warning: simpset does not contain this definition, but separate
        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
 
-primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
+primrec (nonexhaustive) nth :: "'a list => nat => 'a" (infixl "!" 100) where
 nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
   -- {*Warning: simpset does not contain this definition, but separate
        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}