--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -4,7 +4,14 @@
 
 section {*** Type Schemes ***}
 
-thm Set.set_mp Set.subsetD
+datatype foo =
+  Foo1
+| Foo2 bar
+and bar =
+  Bar
+
+ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *}
+
 
 atom_decl name 
 
@@ -16,10 +23,23 @@
 and tys =
   All xs::"name fset" ty::"ty" bind (set+) xs in ty
 
+ML {*
+get_all_info @{context}
+*}
+
+ML {*
+get_info @{context} "TypeSchemes.ty"
+*}
+
+ML {*
+#strong_exhaust (the_info @{context} "TypeSchemes.tys")
+*}
+
 thm ty_tys.distinct
 thm ty_tys.induct
 thm ty_tys.inducts
-thm ty_tys.exhaust ty_tys.strong_exhaust
+thm ty_tys.exhaust 
+thm ty_tys.strong_exhaust
 thm ty_tys.fv_defs
 thm ty_tys.bn_defs
 thm ty_tys.perm_simps
@@ -83,6 +103,7 @@
 apply (subst test3)
 defer
 apply rule*)
+thm subst_substs_graph.intros
 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)