src/HOL/Codatatype/Examples/Misc_Data.thy

--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:40:13 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:40:26 2012 +0200
@@ -52,7 +52,7 @@
  and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
 data_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
-and in_here: 'B = "'b \<times> 'a + 'c"
+     and in_here: 'B = "'b \<times> 'a + 'c"
 
 (* FIXME
 data ('a, 'b, 'c) some_killing =