--- a/src/HOL/Code_Numeral.thy Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Code_Numeral.thy Tue Sep 01 22:32:58 2015 +0200
@@ -10,7 +10,7 @@
subsection \<open>Type of target language integers\<close>
-typedef integer = "UNIV \<Colon> int set"
+typedef integer = "UNIV :: int set"
morphisms int_of_integer integer_of_int ..
setup_lifting type_definition_integer
@@ -615,7 +615,7 @@
subsection \<open>Type of target language naturals\<close>
-typedef natural = "UNIV \<Colon> nat set"
+typedef natural = "UNIV :: nat set"
morphisms nat_of_natural natural_of_nat ..
setup_lifting type_definition_natural