diff -r c53d74b34123 -r 638ed040e6f8 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Thu Mar 13 17:16:49 2014 +0000
+++ b/ProgTutorial/Essential.thy	Thu Apr 03 12:16:56 2014 +0100
@@ -192,8 +192,8 @@
   where a coercion is inserted in the second component and 
 
   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, 
- Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
+  "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>, 
+ Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"}
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the @{text "Trueprop"}-coercion is to embed formulae of