merged

--- a/src/HOL/Matrix/Cplex_tools.ML	Tue Nov 02 16:59:40 2010 +0100
+++ b/src/HOL/Matrix/Cplex_tools.ML	Tue Nov 02 20:32:33 2010 +0100
@@ -977,7 +977,6 @@
     end
     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
      | Option => raise (Load_cplexResult "Option")
-     | x => raise x
 
 fun load_cplexResult name =
     let
@@ -1127,7 +1126,6 @@
     end
     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
      | Option => raise (Load_cplexResult "Option")
-     | x => raise x
 
 exception Execute of string;
 
@@ -1153,7 +1151,7 @@
         result
     end
     handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
-         | _ => raise (Execute answer)
+         | _ => raise (Execute answer)  (* FIXME avoid handle _ *)
     end
 
 fun solve_cplex prog =

--- a/src/HOL/Matrix/matrixlp.ML	Tue Nov 02 16:59:40 2010 +0100
+++ b/src/HOL/Matrix/matrixlp.ML	Tue Nov 02 20:32:33 2010 +0100
@@ -82,7 +82,7 @@
     let
         val simp_th = matrix_compute (cprop_of th)
         val th = Thm.strip_shyps (Thm.equal_elim simp_th th)
-        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle _ => th  (* FIXME avoid handle _ *)
+        fun removeTrue th = removeTrue (Thm.implies_elim th TrueI) handle THM _ => th
     in
         removeTrue th
     end

--- a/src/HOL/ex/Coercion_Examples.thy	Tue Nov 02 16:59:40 2010 +0100
+++ b/src/HOL/ex/Coercion_Examples.thy	Tue Nov 02 20:32:33 2010 +0100
@@ -11,7 +11,7 @@
 
 setup Subtyping.setup
 
-(* Coercion/type maps definitions*)
+(* Error messages test *)
 
 consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
 consts arg :: "int \<Rightarrow> nat"
@@ -36,6 +36,8 @@
 term "[1::int] = func"
 *)
 
+(* Coercion/type maps definitions *)
+
 primrec nat_of_bool :: "bool \<Rightarrow> nat"
 where
   "nat_of_bool False = 0"
@@ -45,17 +47,17 @@
 
 declare [[coercion int]]
 
-declare [[map_function map]]
+declare [[coercion_map map]]
 
 definition map_fun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'd)" where
  "map_fun f g h = g o h o f"
 
-declare [[map_function "\<lambda> f g h . g o h o f"]]
+declare [[coercion_map "\<lambda> f g h . g o h o f"]]
 
 primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
  "map_pair f g (x,y) = (f x, g y)"
 
-declare [[map_function map_pair]]
+declare [[coercion_map map_pair]]
 
 (* Examples taken from the haskell draft implementation *)
 

--- a/src/Tools/subtyping.ML	Tue Nov 02 16:59:40 2010 +0100
+++ b/src/Tools/subtyping.ML	Tue Nov 02 20:32:33 2010 +0100
@@ -762,7 +762,7 @@
   Attrib.setup @{binding coercion}
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_coercion t))))
     "declaration of new coercions" #>
-  Attrib.setup @{binding map_function}
+  Attrib.setup @{binding coercion_map}
     (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
     "declaration of new map functions";