diff -r 31907e0648ee -r 76ccc320b684 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 14:06:17 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 14:06:34 2010 +0100
@@ -202,11 +202,11 @@
   bi::"bp \<Rightarrow> 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
@@ -222,7 +222,7 @@
 | "f (PD (x,y)) = {x,y}"
 
 nominal_datatype trm2 =
-  Var2 "string"
+  Var2 "name"
 | App2 "trm2" "trm2"
 | Lam2 x::"name" t::"trm2"          bindset x in t 
 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
@@ -248,4 +248,4 @@
 
 
 
-end
\ No newline at end of file
+end