Quot/Nominal/Test.thy
changeset 961 0f88e04eb486
parent 954 c009d2535896
child 962 8a16d6c45720
--- 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 \<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
@@ -248,4 +248,4 @@
 
 
 
-end
\ No newline at end of file
+end