src/HOL/Imperative_HOL/ex/SatChecker.thy

--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -119,7 +119,7 @@
 text {* Specific definition for derived clauses in the Array *}
 
 definition
-  array_ran :: "('a\<Colon>heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
+  array_ran :: "('a::heap) option array \<Rightarrow> heap \<Rightarrow> 'a set" where
   "array_ran a h = {e. Some e \<in> set (Array.get h a)}"
     -- {*FIXME*}