--- a/src/HOL/Matrix_LP/Matrix.thy Wed Sep 23 09:50:38 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Thu Sep 24 13:33:42 2015 +0200
@@ -13,7 +13,7 @@
definition "matrix = {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"
-typedef 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
+typedef (overloaded) 'a matrix = "matrix :: (nat \<Rightarrow> nat \<Rightarrow> 'a::zero) set"
unfolding matrix_def
proof
show "(\<lambda>j i. 0) \<in> {(f::(nat \<Rightarrow> nat \<Rightarrow> 'a::zero)). finite (nonzero_positions f)}"