# HG changeset patch
# User blanchet
# Date 1409652812 -7200
# Node ID 3bfd12e456f42decd7ce12703c6e74e3339f9295
# Parent  feb69891e0fdabfb6c1ae9f128945303a407991c# Parent  0774d32fe74f4623b17f6e23ad7d3538984269b2
merge

diff -r feb69891e0fd -r 3bfd12e456f4 src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Sep 02 12:11:04 2014 +0200
+++ b/src/HOL/List.thy	Tue Sep 02 12:13:32 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"} *}