# HG changeset patch
# User wenzelm
# Date 1191182115 -7200
# Node ID 5a3e336a2e371dd1ffe15202a899b61988749632
# Parent  38e5c05ef741ad50c4ce27fa79cf3ad6a95036fb
avoid internal names;

diff -r 38e5c05ef741 -r 5a3e336a2e37 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/Cube/Cube.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -14,7 +14,7 @@
 typedecl typing
 
 nonterminals
-  context_ typing_
+  context' typing'
 
 consts
   Abs           :: "[term, term => term] => term"
@@ -28,13 +28,13 @@
   Has_type      :: "[term, term] => typing"
 
 syntax
-  Trueprop      :: "[context_, typing_] => prop"        ("(_/ |- _)")
-  Trueprop1     :: "typing_ => prop"                    ("(_)")
-  ""            :: "id => context_"                     ("_")
-  ""            :: "var => context_"                    ("_")
-  MT_context    :: "context_"                           ("")
-  Context       :: "[typing_, context_] => context_"    ("_ _")
-  Has_type      :: "[term, term] => typing_"            ("(_:/ _)" [0, 0] 5)
+  Trueprop      :: "[context', typing'] => prop"        ("(_/ |- _)")
+  Trueprop1     :: "typing' => prop"                    ("(_)")
+  ""            :: "id => context'"                     ("_")
+  ""            :: "var => context'"                    ("_")
+  MT_context    :: "context'"                           ("")
+  Context       :: "[typing', context'] => context'"    ("_ _")
+  Has_type      :: "[term, term] => typing'"            ("(_:/ _)" [0, 0] 5)
   Lam           :: "[idt, term, term] => term"          ("(3Lam _:_./ _)" [0, 0, 0] 10)
   Pi            :: "[idt, term, term] => term"          ("(3Pi _:_./ _)" [0, 0] 10)
   arrow         :: "[term, term] => term"               (infixr "->" 10)
@@ -46,7 +46,7 @@
   "A -> B"       => "Prod(A, %_. B)"
 
 syntax (xsymbols)
-  Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
+  Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
   box           :: "term"                               ("\<box>")
   Lam           :: "[idt, term, term] => term"          ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
   Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/AxCompl.thy
--- a/src/HOL/Bali/AxCompl.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/AxCompl.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -1277,7 +1277,7 @@
 	apply (fastsimp intro: eval.Comp) 
 	done
     next
-      case (If_ e c1 c2)
+      case (If' e c1 c2)
       thus "G,A\<turnstile>{=:n} \<langle>If(e) c1 Else c2\<rangle>\<^sub>s\<succ> {G\<rightarrow>}"
 	apply -
 	apply (rule MGFn_NormalI)
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -49,9 +49,9 @@
   "Vals x"     => "(In3 x)"
 
 syntax
-  "Val_"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
-  "Var_"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
-  "Vals_"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
+  "_Val"    :: "[pttrn] => pttrn"     ("Val:_"  [951] 950)
+  "_Var"    :: "[pttrn] => pttrn"     ("Var:_"  [951] 950)
+  "_Vals"   :: "[pttrn] => pttrn"     ("Vals:_" [951] 950)
 
 translations
   "\<lambda>Val:v . b"  == "(\<lambda>v. b) \<circ> the_In1"
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/Conform.thy
--- a/src/HOL/Bali/Conform.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Conform.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -17,7 +17,7 @@
 \end{itemize}
 *}
 
-types	env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+types	env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
 
 
 section "extension of global store"
@@ -388,7 +388,7 @@
 
 constdefs
 
-  conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
+  conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
    "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
     (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
                 \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Decl.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -447,14 +447,14 @@
   subcls1_def: "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: super c = D)}"
 
 syntax
- "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+ "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+ "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+ "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
 
 syntax (xsymbols)
-  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
-  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
-  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
+  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
+  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
+  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
 
 translations
         "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 D" == "(C,D) \<in> subcls1 G"
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -129,11 +129,11 @@
     ultimately show ?case
       by simp
   next
-    case (If_ e c1 c2 jmps' jmps)
-    from If_.prems 
-    have "jumpNestingOkS jmps c1" by - (rule If_.hyps,auto)
-    moreover from If_.prems 
-    have "jumpNestingOkS jmps c2" by - (rule If_.hyps,auto)
+    case (If' e c1 c2 jmps' jmps)
+    from If'.prems 
+    have "jumpNestingOkS jmps c1" by - (rule If'.hyps,auto)
+    moreover from If'.prems 
+    have "jumpNestingOkS jmps c2" by - (rule If'.hyps,auto)
     ultimately show ?case
       by simp
   next
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/Name.thy
--- a/src/HOL/Bali/Name.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Name.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -43,8 +43,8 @@
 
 
 datatype tname	--{* type names for standard classes and other type names *}
-	= Object_
-	| SXcpt_   xname
+	= Object'
+	| SXcpt'   xname
 	| TName   tnam
 
 record   qtname = --{* qualified tname cf. 6.5.3, 6.5.4*}
@@ -90,8 +90,8 @@
   Object :: qtname
   SXcpt  :: "xname \<Rightarrow> qtname"
 defs
-  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object_\<rparr>"
-  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt_ x\<rparr>"
+  Object_def: "Object  \<equiv> \<lparr>pid = java_lang, tid = Object'\<rparr>"
+  SXcpt_def:  "SXcpt   \<equiv> \<lambda>x.  \<lparr>pid = java_lang, tid = SXcpt' x\<rparr>"
 
 lemma Object_neq_SXcpt [simp]: "Object \<noteq> SXcpt xn"
 by (simp add: Object_def SXcpt_def)
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/Term.thy
--- a/src/HOL/Bali/Term.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/Term.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -203,7 +203,7 @@
         | Lab   jump stmt       ("_\<bullet> _" [      99,66]66)
                                 --{* labeled statement; handles break *}
 	| Comp  stmt stmt       ("_;; _"                  [      66,65]65)
-	| If_   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
+	| If'   expr stmt stmt  ("If'(_') _ Else _"       [   80,79,79]70)
 	| Loop  label expr stmt ("_\<bullet> While'(_') _"        [   99,80,79]70)
         | Jmp jump              --{* break, continue, return *}
 	| Throw expr
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/TypeRel.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -37,25 +37,25 @@
 
 syntax
 
- "@subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
- "@subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
+ "_subint1" :: "prog => [qtname, qtname] => bool" ("_|-_<:I1_" [71,71,71] 70)
+ "_subint"  :: "prog => [qtname, qtname] => bool" ("_|-_<=:I _"[71,71,71] 70)
  (* Defined in Decl.thy:
- "@subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
- "@subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
- "@subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
+ "_subcls1" :: "prog => [qtname, qtname] => bool" ("_|-_<:C1_" [71,71,71] 70)
+ "_subclseq":: "prog => [qtname, qtname] => bool" ("_|-_<=:C _"[71,71,71] 70)
+ "_subcls"  :: "prog => [qtname, qtname] => bool" ("_|-_<:C _"[71,71,71] 70)
  *)
  "@implmt1" :: "prog => [qtname, qtname] => bool" ("_|-_~>1_"  [71,71,71] 70)
 
 syntax (xsymbols)
 
-  "@subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
-  "@subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
+  "_subint1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>I1_"  [71,71,71] 70)
+  "_subint"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>I _"  [71,71,71] 70)
   (* Defined in Decl.thy:
-\  "@subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
-  "@subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
-  "@subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
+\  "_subcls1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C\<^sub>1_"  [71,71,71] 70)
+  "_subclseq":: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<preceq>\<^sub>C _"  [71,71,71] 70)
+  "_subcls"  :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<prec>\<^sub>C _"  [71,71,71] 70)
   *)
-  "@implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
+  "_implmt1" :: "prog \<Rightarrow> [qtname, qtname] \<Rightarrow> bool" ("_\<turnstile>_\<leadsto>1_"  [71,71,71] 70)
 
 translations
 
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/TypeSafe.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -97,7 +97,7 @@
 section "result conformance"
 
 constdefs
-  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env_ \<Rightarrow> bool"
+  assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool"
           ("_\<le>|_\<preceq>_\<Colon>\<preceq>_"                                        [71,71,71,71] 70)
 "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
  (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Bali/WellType.thy
--- a/src/HOL/Bali/WellType.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Bali/WellType.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -426,19 +426,19 @@
 
 
 syntax (* for purely static typing *)
-  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
-  wt_stmt_ :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
-  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
-  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
-  ty_exprs_:: "env \<Rightarrow> [expr list,
+  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
+  "_wt_stmt" :: "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_|-_:<>" [51,51   ] 50)
+  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
+  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
+  "_ty_exprs":: "env \<Rightarrow> [expr list,
 		     \<spacespace> ty   list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
 
 syntax (xsymbols)
-  wt_      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
-  wt_stmt_ ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
-  ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
-  ty_var_  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
-  ty_exprs_ :: "env \<Rightarrow> [expr list,
+  "_wt"      :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_"  [51,51,51] 50)
+  "_wt_stmt" ::  "env \<Rightarrow>  stmt       \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>"  [51,51   ] 50)
+  "_ty_expr" :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
+  "_ty_var"  :: "env \<Rightarrow> [var  ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
+  "_ty_exprs" :: "env \<Rightarrow> [expr list,
 		    \<spacespace>  ty   list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
 
 translations
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -1908,7 +1908,7 @@
   from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
   from uset_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
   from U_l UpU 
-  have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+  have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
   hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
     by (auto simp add: mult_pos_pos)
   have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0" 
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MetisExamples/Abstraction.thy
--- a/src/HOL/MetisExamples/Abstraction.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -94,10 +94,10 @@
 proof (neg_clausify)
 assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
    (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
-   Collect (llabs_Set_XCollect_ex_eq_3_ op \<in> (pset cl))"
+   Collect (llabs_Set_XCollect_ex_eq_3 op \<in> (pset cl))"
 assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
 assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
-have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
+have 3: "llabs_Predicate_Xsup_Un_eq2_1 (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
  (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
   by (metis acc_def 2)
 assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
@@ -120,7 +120,7 @@
 assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
    (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
    Collect
-    (llabs_Set_XCollect_ex_eq_3_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
+    (llabs_Set_XCollect_ex_eq_3 op \<in> (Pi (pset cl) (COMBK (pset cl))))"
 assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
 assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
 \<in> Sigma (CL\<Colon>'a\<Colon>type set set)
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/Conform.thy
--- a/src/HOL/MicroJava/J/Conform.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Conform.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -8,7 +8,7 @@
 
 theory Conform imports State WellType Exceptions begin
 
-types 'c env_ = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
+types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
 
 constdefs
 
@@ -32,7 +32,7 @@
   xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool"
   "xconf hp vo  == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
 
-  conforms :: "xstate => java_mb env_ => bool" ("_ ::<= _" [51,51] 50)
+  conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50)
  "s::<=E == prg E|-h heap (store s) [ok] \<and> 
             prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> 
             xconf (heap (store s)) (abrupt s)"
@@ -54,7 +54,7 @@
   hconf    :: "'c prog => aheap => bool"
               ("_ \<turnstile>h _ \<surd>" [51,51] 50)
 
-  conforms :: "state => java_mb env_ => bool"
+  conforms :: "state => java_mb env' => bool"
               ("_ ::\<preceq> _" [51,51] 50)
 
 
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -37,23 +37,23 @@
 \end{verbatim}
 *}
 
-datatype cnam_ = Base_ | Ext_
-datatype vnam_ = vee_ | x_ | e_
+datatype cnam' = Base' | Ext'
+datatype vnam' = vee' | x' | e'
 
 consts
-  cnam_ :: "cnam_ => cname"
-  vnam_ :: "vnam_ => vnam"
+  cnam' :: "cnam' => cname"
+  vnam' :: "vnam' => vnam"
 
--- "@{text cnam_} and @{text vnam_} are intended to be isomorphic 
+-- "@{text cnam'} and @{text vnam'} are intended to be isomorphic 
     to @{text cnam} and @{text vnam}"
 axioms 
-  inj_cnam_:  "(cnam_ x = cnam_ y) = (x = y)"
-  inj_vnam_:  "(vnam_ x = vnam_ y) = (x = y)"
+  inj_cnam':  "(cnam' x = cnam' y) = (x = y)"
+  inj_vnam':  "(vnam' x = vnam' y) = (x = y)"
 
-  surj_cnam_: "\<exists>m. n = cnam_ m"
-  surj_vnam_: "\<exists>m. n = vnam_ m"
+  surj_cnam': "\<exists>m. n = cnam' m"
+  surj_vnam': "\<exists>m. n = vnam' m"
 
-declare inj_cnam_ [simp] inj_vnam_ [simp]
+declare inj_cnam' [simp] inj_vnam' [simp]
 
 syntax
   Base :: cname
@@ -63,11 +63,11 @@
   e    :: vname
 
 translations
-  "Base" == "cnam_ Base_"
-  "Ext"  == "cnam_ Ext_"
-  "vee"  == "VName (vnam_ vee_)"
-  "x"  == "VName (vnam_ x_)"
-  "e"  == "VName (vnam_ e_)"
+  "Base" == "cnam' Base'"
+  "Ext"  == "cnam' Ext'"
+  "vee"  == "VName (vnam' vee')"
+  "x"  == "VName (vnam' x')"
+  "e"  == "VName (vnam' e')"
 
 axioms
   Base_not_Object: "Base \<noteq> Object"
@@ -220,52 +220,52 @@
 
 declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
 
-lemma acyclic_subcls1_: "acyclicP (subcls1 tprg)"
+lemma acyclic_subcls1': "acyclicP (subcls1 tprg)"
 apply (rule acyclicI [to_pred])
 apply safe
 done
 
-lemmas wf_subcls1_ = acyclic_subcls1_ [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
+lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse [to_pred]]]
 
-lemmas fields_rec_ = wf_subcls1_ [THEN [2] fields_rec_lemma]
+lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma]
 
 lemma fields_Object [simp]: "fields (tprg, Object) = []"
-apply (subst fields_rec_)
+apply (subst fields_rec')
 apply   auto
 done
 
 declare is_class_def [simp]
 
 lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
-apply (subst fields_rec_)
+apply (subst fields_rec')
 apply   auto
 done
 
 lemma fields_Ext [simp]: 
   "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
 apply (rule trans)
-apply  (rule fields_rec_)
+apply  (rule fields_rec')
 apply   auto
 done
 
-lemmas method_rec_ = wf_subcls1_ [THEN [2] method_rec_lemma]
+lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma]
 
 lemma method_Object [simp]: "method (tprg,Object) = map_of []"
-apply (subst method_rec_)
+apply (subst method_rec')
 apply  auto
 done
 
 lemma method_Base [simp]: "method (tprg, Base) = map_of  
   [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
 apply (rule trans)
-apply  (rule method_rec_)
+apply  (rule method_rec')
 apply  auto
 done
 
 lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
   [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
 apply (rule trans)
-apply  (rule method_rec_)
+apply  (rule method_rec')
 apply  auto
 done
 
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/JBasis.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -56,14 +56,14 @@
 apply  auto
 done
 
-lemma Ball_set_table_: 
+lemma Ball_set_table': 
   "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
 apply(induct_tac "l")
 apply(simp_all (no_asm))
 apply safe
 apply auto
 done
-lemmas Ball_set_table = Ball_set_table_ [THEN mp];
+lemmas Ball_set_table = Ball_set_table' [THEN mp];
 
 lemma table_of_remap_SomeD [rule_format (no_asm)]: 
 "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> 
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -62,7 +62,7 @@
   cname ("string")
   vnam ("string")
   mname ("string")
-  loc_ ("int")
+  loc' ("int")
 
 consts_code
   "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/State.thy
--- a/src/HOL/MicroJava/J/State.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/State.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -9,9 +9,9 @@
 theory State imports TypeRel Value begin
 
 types 
-  fields_ = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
+  fields' = "(vname \<times> cname \<rightharpoonup> val)"  -- "field name, defining class, value"
 
-  obj = "cname \<times> fields_"    -- "class instance with class name and fields"
+  obj = "cname \<times> fields'"    -- "class instance with class name and fields"
 
 constdefs
   obj_ty  :: "obj => ty"
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/J/Value.thy
--- a/src/HOL/MicroJava/J/Value.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/J/Value.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -8,11 +8,11 @@
 
 theory Value imports Type begin
 
-typedecl loc_ -- "locations, i.e. abstract references on objects" 
+typedecl loc' -- "locations, i.e. abstract references on objects" 
 
 datatype loc 
   = XcptRef xcpt -- "special locations for pre-allocated system exceptions"
-  | Loc loc_     -- "usual locations (references on objects)"
+  | Loc loc'     -- "usual locations (references on objects)"
 
 datatype val
   = Unit        -- "dummy result value of void methods"
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/HOL/MicroJava/JVM/JVMListExample.thy
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -91,7 +91,7 @@
   cnam ("string")
   vnam ("string")
   mname ("string")
-  loc_ ("int")
+  loc' ("int")
 
 consts_code
   "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
diff -r 38e5c05ef741 -r 5a3e336a2e37 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Sun Sep 30 16:53:08 2007 +0200
+++ b/src/ZF/AC/WO6_WO1.thy	Sun Sep 30 21:55:15 2007 +0200
@@ -75,13 +75,13 @@
 lemma lam_sets: "f \<in> A->B ==> (\<lambda>x \<in> A. {f`x}): A -> {{b}. b \<in> B}"
 by (fast intro!: lam_type apply_type)
 
-lemma surj_imp_eq_: "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
+lemma surj_imp_eq': "f \<in> surj(A,B) ==> (\<Union>a \<in> A. {f`a}) = B"
 apply (unfold surj_def)
 apply (fast elim!: apply_type)
 done
 
 lemma surj_imp_eq: "[| f \<in> surj(A,B); Ord(A) |] ==> (\<Union>a<A. {f`a}) = B"
-by (fast dest!: surj_imp_eq_ intro!: ltI elim!: ltE)
+by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
 
 lemma WO1_WO4: "WO1 ==> WO4(1)"
 apply (unfold WO1_def WO4_def)