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/Comp/DefsComp.thy
changeset 77645 7edbb16bc60f
parent 68451 c34aa23a1fb6 
--- a/src/HOL/MicroJava/Comp/DefsComp.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -65,7 +65,7 @@
 
 definition locals_locvars :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> locvars \<Rightarrow> State.locals" where
   "locals_locvars G C S lvs == 
-  Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs)) (This\<mapsto>(hd lvs))"
+  Map.empty ((gjmb_plns (gmb G C S))[\<mapsto>](tl lvs), This\<mapsto>(hd lvs))"
 
 definition locvars_xstate :: "java_mb prog \<Rightarrow> cname \<Rightarrow> sig \<Rightarrow> xstate \<Rightarrow> locvars" where
   "locvars_xstate G C S xs == locvars_locals G C S (gl xs)"
isabelle