# HG changeset patch
# User wenzelm
# Date 1437245585 -7200
# Node ID 80ca4a065a48d732d7e783806af4f741b62ab527
# Parent  b48830b670a1c7351dae9ae4ce9514ecb117dbac
tuned whitespace;

diff -r b48830b670a1 -r 80ca4a065a48 src/HOL/HOLCF/Domain.thy
--- 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"