# HG changeset patch
# User Andreas Lochbihler
# Date 1375978512 -7200
# Node ID 5f3faf72b62a43e7ac94789a2dbfa921aaf576c0
# Parent  7bfe0df532a9d11f26d2353583b355b721b74af3
prefer Code.abort with explicit error message

diff -r 7bfe0df532a9 -r 5f3faf72b62a src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/Library/FinFun.thy	Thu Aug 08 18:15:12 2013 +0200
@@ -17,13 +17,6 @@
 *}
 
 
-definition "code_abort" :: "(unit \<Rightarrow> 'a) \<Rightarrow> 'a"
-where [simp, code del]: "code_abort f = f ()"
-
-code_abort "code_abort"
-
-hide_const (open) "code_abort"
-
 subsection {* The @{text "map_default"} operation *}
 
 definition map_default :: "'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
@@ -1284,7 +1277,7 @@
 
 lemma finfun_dom_const_code [code]:
   "finfun_dom ((K$ c) :: ('a :: card_UNIV) \<Rightarrow>f 'b) = 
-   (if CARD('a) = 0 then (K$ False) else FinFun.code_abort (\<lambda>_. finfun_dom (K$ c)))"
+   (if CARD('a) = 0 then (K$ False) else Code.abort (STR ''finfun_dom called on finite type'') (\<lambda>_. finfun_dom (K$ c)))"
 by(simp add: finfun_dom_const card_UNIV card_eq_0_iff)
 
 lemma finfun_dom_finfunI: "(\<lambda>a. f $ a \<noteq> finfun_default f) \<in> finfun"
@@ -1347,7 +1340,7 @@
 
 lemma finfun_to_list_const_code [code]:
   "finfun_to_list ((K$ c) :: ('a :: {linorder, card_UNIV} \<Rightarrow>f 'b)) =
-   (if CARD('a) = 0 then [] else FinFun.code_abort (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
+   (if CARD('a) = 0 then [] else Code.abort (STR ''finfun_to_list called on finite type'') (\<lambda>_. finfun_to_list ((K$ c) :: ('a \<Rightarrow>f 'b))))"
 by(auto simp add: finfun_to_list_const card_UNIV card_eq_0_iff)
 
 lemma remove1_insort_insert_same:
diff -r 7bfe0df532a9 -r 5f3faf72b62a src/HOL/ex/FinFunPred.thy
--- a/src/HOL/ex/FinFunPred.thy	Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/ex/FinFunPred.thy	Thu Aug 08 18:15:12 2013 +0200
@@ -133,11 +133,11 @@
 where [code del]: "finfun_Ball_except xs A P = (\<forall>a. A $ a \<longrightarrow> a \<in> set xs \<or> P a)"
 
 lemma finfun_Ball_except_const:
-  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
+  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
 by(auto simp add: finfun_Ball_except_def)
 
 lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
-  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> FinFun.code_abort (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
+  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
 by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)
 
 lemma finfun_Ball_except_update:
@@ -160,11 +160,11 @@
 where [code del]: "finfun_Bex_except xs A P = (\<exists>a. A $ a \<and> a \<notin> set xs \<and> P a)"
 
 lemma finfun_Bex_except_const:
-  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
+  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
 by(auto simp add: finfun_Bex_except_def)
 
 lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
-  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> FinFun.code_abort (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
+  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
 by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)
 
 lemma finfun_Bex_except_update: