--- a/ProgTutorial/First_Steps.thy	Thu Oct 27 18:11:52 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Sat Oct 29 12:17:06 2011 +0100
@@ -662,14 +662,6 @@
   ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
 *}
 
-ML {*
-  val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) = 
-  @{context}
-  |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
-  ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
 
 text {*
   Recall that @{ML "|>"} is the reverse function application. Recall also that