src/HOL/Library/Numeral_Type.thy
changeset 52147 9943f8067f11
parent 52143 36ffe23b25f8
child 55142 378ae9e46175
--- a/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:13:34 2013 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Sat May 25 17:40:44 2013 +0200
@@ -519,7 +519,8 @@
       | bit_tr' b _ = raise Match;
   in
    [(@{type_syntax bit0}, K (bit_tr' 0)),
-    (@{type_syntax bit1}, K (bit_tr' 1))] end;
+    (@{type_syntax bit1}, K (bit_tr' 1))]
+  end;
 *}
 
 subsection {* Examples *}