# HG changeset patch
# User wenzelm
# Date 1206642143 -3600
# Node ID 158b924b51531a9f76c4e3db3f95e79355d74fa4
# Parent  28310714259201c26ee274f12506af345894d04b
avoid amiguity of State.state vs. JVMType.state;

diff -r 283107142592 -r 158b924b5153 src/HOL/MicroJava/BV/Altern.thy
--- a/src/HOL/MicroJava/BV/Altern.thy	Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/Altern.thy	Thu Mar 27 19:22:23 2008 +0100
@@ -12,7 +12,7 @@
 
 
 constdefs
-  check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"
+  check_type :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state \<Rightarrow> bool"
   "check_type G mxs mxr s \<equiv> s \<in> states G mxs mxr"
 
   wt_instr_altern :: "[instr,jvm_prog,ty,method_type,nat,nat,p_count,
diff -r 283107142592 -r 158b924b5153 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Thu Mar 27 19:22:23 2008 +0100
@@ -11,7 +11,7 @@
 
 constdefs
   kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
-             instr list \<Rightarrow> state list \<Rightarrow> state list"
+             instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list"
   "kiljvm G maxs maxr rT et bs ==
   kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)"
 
diff -r 283107142592 -r 158b924b5153 src/HOL/MicroJava/BV/LBVJVM.thy
--- a/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/LBVJVM.thy	Thu Mar 27 19:22:23 2008 +0100
@@ -10,20 +10,20 @@
 imports LBVCorrect LBVComplete Typing_Framework_JVM
 begin
 
-types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> state list"
+types prog_cert = "cname \<Rightarrow> sig \<Rightarrow> JVMType.state list"
 
 constdefs
-  check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
+  check_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> JVMType.state list \<Rightarrow> bool"
   "check_cert G mxs mxr n cert \<equiv> check_types G mxs mxr cert \<and> length cert = n+1 \<and>
                                  (\<forall>i<n. cert!i \<noteq> Err) \<and> cert!n = OK None"
 
   lbvjvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> 
-             state list \<Rightarrow> instr list \<Rightarrow> state \<Rightarrow> state"
+             JVMType.state list \<Rightarrow> instr list \<Rightarrow> JVMType.state \<Rightarrow> JVMType.state"
   "lbvjvm G maxs maxr rT et cert bs \<equiv>
   wtl_inst_list bs cert  (JVMType.sup G maxs maxr) (JVMType.le G maxs maxr) Err (OK None) (exec G maxs rT et bs) 0"
 
   wt_lbv :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
-             exception_table \<Rightarrow> state list \<Rightarrow> instr list \<Rightarrow> bool"
+             exception_table \<Rightarrow> JVMType.state list \<Rightarrow> instr list \<Rightarrow> bool"
   "wt_lbv G C pTs rT mxs mxl et cert ins \<equiv>
    check_bounded ins et \<and> 
    check_cert G mxs (1+size pTs+mxl) (length ins) cert \<and>
@@ -37,7 +37,7 @@
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_lbv G C (snd sig) rT maxs maxl et (cert C sig) b) G"
 
   mk_cert :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list 
-              \<Rightarrow> method_type \<Rightarrow> state list"
+              \<Rightarrow> method_type \<Rightarrow> JVMType.state list"
   "mk_cert G maxs rT et bs phi \<equiv> make_cert (exec G maxs rT et bs) (map OK phi) (OK None)"
 
   prg_cert :: "jvm_prog \<Rightarrow> prog_type \<Rightarrow> prog_cert"
diff -r 283107142592 -r 158b924b5153 src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 27 19:05:10 2008 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 27 19:22:23 2008 +0100
@@ -10,7 +10,7 @@
 
 
 constdefs
-  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state step_type"
+  exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state step_type"
   "exec G maxs rT et bs == 
   err_step (size bs) (\<lambda>pc. app (bs!pc) G maxs rT pc et) (\<lambda>pc. eff (bs!pc) G pc et)"