diff -r 23a8c5ac35f8 -r 69916a850301 src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/MicroJava/Comp/Index.thy
-    ID:         $Id$
     Author:     Martin Strecker
 *)
 
@@ -105,7 +104,7 @@
 (* This corresponds to the original def in wf_java_mdecl:
   "disjoint_varnames pns lvars \<equiv> 
   nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
-	(\<forall>pn\<in>set pns. map_of lvars pn = None)"
+        (\<forall>pn\<in>set pns. map_of lvars pn = None)"
 *)
 
   "disjoint_varnames pns lvars \<equiv>