src/HOL/Induct/LList.thy

--- a/src/HOL/Induct/LList.thy	Mon Oct 26 15:36:50 2009 +0100
+++ b/src/HOL/Induct/LList.thy	Mon Oct 26 20:02:37 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Induct/LList.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Shares NIL, CONS, List_case with List.thy
@@ -906,8 +905,8 @@
 by (rule_tac l = l1 in llist_fun_equalityI, auto)
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
-                            (map dest_Const [@{term LNil}, @{term LCons}])
+  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+    (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 end