--- a/Nominal/Test.thy	Tue Mar 23 08:33:48 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 23 08:42:02 2010 +0100
@@ -1,88 +1,10 @@
 theory Test
-imports "Parser" "../Attic/Prove"
+imports "Parser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
-
-text {* example 1, equivalent to example 2 from Terms *}
-
-nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam" bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
-and bp =
-  BP "name" "lam"
-binder
-  bi::"bp \<Rightarrow> atom set"
-where
-  "bi (BP x t) = {atom x}"
-
-thm lam_bp.fv
-thm lam_bp.supp
-thm lam_bp.eq_iff
-thm lam_bp.bn
-thm lam_bp.perm
-thm lam_bp.induct
-thm lam_bp.inducts
-thm lam_bp.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
-
-ML {* val _ = recursive := true *}
-
-nominal_datatype lam' =
-  VAR' "name"
-| APP' "lam'" "lam'"
-| LAM' x::"name" t::"lam'"  bind x in t
-| LET' bp::"bp'" t::"lam'"   bind "bi' bp" in t
-and bp' =
-  BP' "name" "lam'"
-binder
-  bi'::"bp' \<Rightarrow> atom set"
-where
-  "bi' (BP' x t) = {atom x}"
-
-thm lam'_bp'.fv
-thm lam'_bp'.eq_iff[no_vars]
-thm lam'_bp'.bn
-thm lam'_bp'.perm
-thm lam'_bp'.induct
-thm lam'_bp'.inducts
-thm lam'_bp'.distinct
-ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
-
-thm lam'_bp'.fv[simplified lam'_bp'.supp]
-
-
-text {* example 2 *}
-
 ML {* val _ = recursive := false  *}
-nominal_datatype trm' =
-  Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'"          bind x in t
-| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
-and pat' =
-  PN
-| PS "name"
-| PD "name" "name"
-binder
-  f::"pat' \<Rightarrow> atom set"
-where
-  "f PN = {}"
-| "f (PD x y) = {atom x, atom y}"
-| "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
 
 nominal_datatype trm0 =
   Var0 "name"
@@ -444,19 +366,6 @@
 | "bv8 (Bar1 v x b) = {atom v}"
 *)
 
-(* Type schemes with separate datatypes *)
-nominal_datatype T =
-  TVar "name"
-| TFun "T" "T"
-
-(* PROBLEM: 
-*** exception Datatype raised 
-*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML")
-*** At command "nominal_datatype".
-nominal_datatype TyS =
-  TAll xs::"name list" ty::"T" bind xs in ty
-*)
-
 (* example 9 from Peter Sewell's bestiary *)
 (* run out of steam at the moment *)