Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/JVM/JVMExecInstr.thy
changeset 28524 644b62cf678f
parent 16417 9bc16273c2d4
child 39758 b8a53e3a0ee2 
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Oct 07 16:07:50 2008 +0200
@@ -66,7 +66,7 @@
        dynT = fst(the(hp(the_Addr oref)));
        (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
        frs' = if xp'=None then 
-                [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+                [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
               else []
    in 
       (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))"
isabelle