--- a/src/HOL/HOLCF/Domain.thy Sat Jul 18 20:47:08 2015 +0200
+++ b/src/HOL/HOLCF/Domain.thy Sat Jul 18 20:53:05 2015 +0200
@@ -142,12 +142,12 @@
setup {*
fold Sign.add_const_constraint
- [ (@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"})
- , (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"})
- , (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"})
- , (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"})
- , (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"})
- , (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"}) ]
+ [(@{const_name defl}, SOME @{typ "'a::domain itself \<Rightarrow> udom defl"}),
+ (@{const_name emb}, SOME @{typ "'a::domain \<rightarrow> udom"}),
+ (@{const_name prj}, SOME @{typ "udom \<rightarrow> 'a::domain"}),
+ (@{const_name liftdefl}, SOME @{typ "'a::predomain itself \<Rightarrow> udom u defl"}),
+ (@{const_name liftemb}, SOME @{typ "'a::predomain u \<rightarrow> udom u"}),
+ (@{const_name liftprj}, SOME @{typ "udom u \<rightarrow> 'a::predomain u"})]
*}
ML_file "Tools/domaindef.ML"