diff -r 7eff23d0b380 -r c26964691975 src/HOL/MicroJava/JVM/Opstack.thy
--- a/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 15:38:42 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Opstack.thy	Thu Jul 06 15:58:40 2000 +0200
@@ -17,7 +17,7 @@
  | Dup_x1
  | Dup_x2
  | Swap
- | ADD
+ | IAdd
 	  
 consts
  exec_os :: "[op_stack,opstack,p_count] \\<Rightarrow> (opstack \\<times> p_count)" 
@@ -36,7 +36,7 @@
 	 in
 	 (val2#val1#(tl (tl stk)) , pc+1))"
 
-  "exec_os ADD stk pc =
+  "exec_os IAdd stk pc =
   (let (val1,val2) = (hd stk,hd (tl stk))
    in
    (Intg ((the_Intg val1)+(the_Intg val2))#(tl (tl stk)), pc+1))"