diff -r 957f69b9b7df -r f952f2679a11 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/Essential.thy	Sat Aug 28 13:27:16 2010 +0800
@@ -1438,14 +1438,14 @@
   val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
 
   val Pt_implies_Qt = 
-        assume assm1
-        |> forall_elim @{cterm "t::nat"}
+        Thm.assume assm1
+        |> Thm.forall_elim @{cterm "t::nat"}
   
-  val Qt = implies_elim Pt_implies_Qt (assume assm2)
+  val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
 in
   Qt 
-  |> implies_intr assm2
-  |> implies_intr assm1
+  |> Thm.implies_intr assm2
+  |> Thm.implies_intr assm1
 end*}
 
 text {*