# HG changeset patch
# User wenzelm
# Date 1441790674 -7200
# Node ID 6d29eb7c5fb283be8cd68cb307a94429ca25d12d
# Parent  f9fd43d8981daa767460b85de25efd38d38512a4
eliminated \<Colon> -- from dead code!

diff -r f9fd43d8981d -r 6d29eb7c5fb2 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Tue Sep 08 21:57:18 2015 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Wed Sep 09 11:24:34 2015 +0200
@@ -291,7 +291,7 @@
 
 definition "scalar_product v w = (\<Sum> (x, y)\<leftarrow>zip v w. x * y)"
 
-definition mv :: "('a \<Colon> semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+definition mv :: "('a :: semiring_0) list list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   where [simp]: "mv M v = map (scalar_product v) M"
 text {*
   This defines the matrix vector multiplication. To work properly @{term
@@ -306,7 +306,7 @@
   by (auto simp: sparsify_def set_zip)
 
 lemma listsum_sparsify[simp]:
-  fixes v :: "('a \<Colon> semiring_0) list"
+  fixes v :: "('a :: semiring_0) list"
   assumes "length w = length v"
   shows "(\<Sum>x\<leftarrow>sparsify w. (\<lambda>(i, x). v ! i) x * snd x) = scalar_product v w"
     (is "(\<Sum>x\<leftarrow>_. ?f x) = _")
@@ -316,11 +316,11 @@
 *)
 definition [simp]: "unzip w = (map fst w, map snd w)"
 
-primrec insert :: "('a \<Rightarrow> 'b \<Colon> linorder) => 'a \<Rightarrow> 'a list => 'a list" where
+primrec insert :: "('a \<Rightarrow> 'b :: linorder) => 'a \<Rightarrow> 'a list => 'a list" where
   "insert f x [] = [x]" |
   "insert f x (y # ys) = (if f y < f x then y # insert f x ys else x # y # ys)"
 
-primrec sort :: "('a \<Rightarrow> 'b \<Colon> linorder) \<Rightarrow> 'a list => 'a list" where
+primrec sort :: "('a \<Rightarrow> 'b :: linorder) \<Rightarrow> 'a list => 'a list" where
   "sort f [] = []" |
   "sort f (x # xs) = insert f x (sort f xs)"