diff -r fa4ebbd350ae -r 4645502c3c64 src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Oct 06 13:31:44 2015 +0200
+++ b/src/HOL/Bali/Example.thy	Tue Oct 06 15:14:28 2015 +0200
@@ -1078,7 +1078,7 @@
 
 subsubsection "well-typedness"
 
-schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
+schematic_goal wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
 apply (unfold test_def arr_viewed_from_def)
 (* ?pTs = [Class Base] *)
 apply (rule wtIs (* ;; *))
@@ -1130,7 +1130,7 @@
 
 subsubsection "definite assignment"
 
-schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
+schematic_goal da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
                   \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
 apply (unfold test_def arr_viewed_from_def)
 apply (rule da.Comp)
@@ -1248,7 +1248,7 @@
 
 
 declare Pair_eq [simp del]
-schematic_lemma exec_test: 
+schematic_goal exec_test: 
 "\<lbrakk>the (new_Addr (heap  s1)) = a;  
   the (new_Addr (heap ?s2)) = b;  
   the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>