diff -r 9911824a5396 -r ed89a26b7074 Nominal/ExTySch.thy --- a/Nominal/ExTySch.thy Sat Mar 27 06:51:13 2010 +0100 +++ b/Nominal/ExTySch.thy Sat Mar 27 08:11:11 2010 +0100 @@ -5,6 +5,7 @@ (* Type Schemes *) atom_decl name +(*ML {* val _ = alpha_type := AlphaRes *}*) nominal_datatype t = Var "name" | Fun "t" "t"