--- a/ProgTutorial/FirstSteps.thy	Fri Apr 03 07:55:07 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Tue Apr 07 17:04:39 2009 +0100
@@ -1554,6 +1554,68 @@
   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 () = warning (concat [s1, " ", s2, " ", s3, "\n"])
+   end*}
+
+ML_val{*structure t = Test(U) *} 
+
+ML_val{*structure Datatab = TableFun(type key = int val ord = int_ord);*}
+
 section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}