diff -r 188826f1ccdb -r 7bc38b93a1fc Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Mon Mar 24 15:31:17 2014 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy	Sun Apr 06 13:07:24 2014 +0100
@@ -68,6 +68,7 @@
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+thm subst_substs_graph_def subst_substs_graph_aux_def
 apply(simp add: subst_substs_graph_aux_def eqvt_def)
 apply(rule TrueI)
 apply (case_tac x)