diff -r d7ec7b1204a5 -r 0f88e04eb486 Quot/Nominal/Test.thy --- a/Quot/Nominal/Test.thy Wed Jan 27 12:21:40 2010 +0100 +++ b/Quot/Nominal/Test.thy Wed Jan 27 13:32:28 2010 +0100 @@ -202,11 +202,11 @@ bi::"bp \ name set" where "bi (BP x t) = {x}" - +print_theorems text {* examples 2 *} nominal_datatype trm = - Var "string" + Var "name" | App "trm" "trm" | Lam x::"name" t::"trm" bindset x in t | Let p::"pat" "trm" t::"trm" bind "f p" in t @@ -248,4 +248,4 @@ -end \ No newline at end of file +end