--- 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>