# HG changeset patch
# User haftmann
# Date 1179567206 -7200
# Node ID 9872ef956276c07a1ef6486bb0c60edbbfd30665
# Parent  f602a131eaa15c634a414cb62efdbfebfcee4d39
added qualification for ambiguous definition names

diff -r f602a131eaa1 -r 9872ef956276 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sat May 19 11:33:26 2007 +0200
@@ -5,7 +5,9 @@
 
 header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
 
-theory BVExample imports JVMListExample BVSpecTypeSafe JVM ExecutableSet begin
+theory BVExample
+imports JVMListExample BVSpecTypeSafe JVM ExecutableSet
+begin
 
 text {*
   This theory shows type correctness of the example program in section 
@@ -115,7 +117,7 @@
 
 lemma field_val [simp]:
   "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
-  apply (unfold field_def)
+  apply (unfold TypeRel.field_def)
   apply (insert class_list)
   apply (unfold list_class_def)
   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
@@ -124,7 +126,7 @@
 
 lemma field_next [simp]:
   "field (E, list_name) next_name = Some (list_name, Class list_name)"
-  apply (unfold field_def)
+  apply (unfold TypeRel.field_def)
   apply (insert class_list)
   apply (unfold list_class_def)
   apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
diff -r f602a131eaa1 -r 9872ef956276 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sat May 19 11:33:26 2007 +0200
@@ -1237,7 +1237,7 @@
 apply simp+
 apply (simp only: comp_is_type)
 apply (rule_tac C=cname in fields_is_type)
-apply (simp add: field_def)
+apply (simp add: TypeRel.field_def)
 apply (drule JBasis.table_of_remap_SomeD)+
 apply assumption+
 apply (erule wf_prog_ws_prog)
diff -r f602a131eaa1 -r 9872ef956276 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat May 19 11:33:25 2007 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sat May 19 11:33:26 2007 +0200
@@ -5,7 +5,9 @@
 
 (* Lemmas for compiler correctness proof *)
 
-theory LemmasComp imports TranslComp begin
+theory LemmasComp
+imports TranslComp
+begin
 
 
 declare split_paired_All [simp del]
@@ -222,7 +224,7 @@
 
 lemma comp_field: "wfP ((subcls1 G)^--1) \<Longrightarrow> 
   field (comp G,C) = field (G,C)" 
-by (simp add: field_def comp_fields)
+by (simp add: TypeRel.field_def comp_fields)