diff -r 2b7c08d90e2e -r 92f6a772e013 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Tue Aug 25 00:07:37 2009 +0200
+++ b/ProgTutorial/General.thy	Mon Sep 28 01:21:27 2009 +0200
@@ -2,7 +2,7 @@
 imports Base FirstSteps
 begin
 
-chapter {* General Infrastructure *}
+chapter {* Isabelle -- The Good, the Bad and the Ugly *}
 
 text {*
   Isabelle is build around a few central ideas. One is the LCF-approach to
@@ -1244,73 +1244,6 @@
   valid local theory.
 *}
 
-(*
-ML{*signature UNIVERSAL_TYPE =
-sig
-  type t
-
-  val embed: unit -> ('a -> t) * (t -> 'a option)
-end*}
-
-ML{*structure U:> UNIVERSAL_TYPE =
-   struct
-      type t = exn
-
-      fun 'a embed () =
-         let
-            exception E of 'a
-            fun project (e: t): 'a option =
-               case e of
-                  E a => SOME a
-                | _ => NONE
-         in
-            (E, project)
-         end
-   end*}
-
-text {*
-  The idea is that type t is the universal type and that each call to embed
-  returns a new pair of functions (inject, project), where inject embeds a
-  value into the universal type and project extracts the value from the
-  universal type. A pair (inject, project) returned by embed works together in
-  that project u will return SOME v if and only if u was created by inject
-  v. If u was created by a different function inject', then project returns
-  NONE.
-
-  in library.ML
-*}
-
-ML_val{*structure Object = struct type T = exn end; *}
-
-ML{*functor Test (U: UNIVERSAL_TYPE): sig end =
-   struct
-      val (intIn: int -> U.t, intOut) = U.embed ()
-      val r: U.t ref = ref (intIn 13)
-      val s1 =
-         case intOut (!r) of
-            NONE => "NONE"
-          | SOME i => Int.toString i
-      val (realIn: real -> U.t, realOut) = U.embed ()
-      val () = r := realIn 13.0
-      val s2 =
-         case intOut (!r) of
-            NONE => "NONE"
-          | SOME i => Int.toString i
-      val s3 =
-         case realOut (!r) of
-            NONE => "NONE"
-          | SOME x => Real.toString x
-      val () = tracing (concat [s1, " ", s2, " ", s3, "\n"])
-   end*}
-
-ML_val{*structure t = Test(U) *} 
-
-ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
-
-ML {* LocalTheory.restore *}
-ML {* LocalTheory.set_group *}
-*)
-
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML_ind  add_thms_dynamic in PureThy} *}