--- a/Nominal/TySch.thy	Tue Mar 23 08:33:48 2010 +0100
+++ b/Nominal/TySch.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -147,4 +147,19 @@
   apply auto
   done
 
+(* PROBLEM:
+Type schemes with separate datatypes
+
+nominal_datatype T =
+  TVar "name"
+| TFun "T" "T"
+nominal_datatype TyS =
+  TAll xs::"name list" ty::"T" bind xs in ty
+
+*** exception Datatype raised
+*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
+*** At command "nominal_datatype".
+*)
+
+
 end