# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264595548 -3600
# Node ID 0f88e04eb486142733bba1cf7b5813db41d90e94
# Parent  d7ec7b1204a542b3d71fde486c0b7c07af7f40ea
Variable takes a 'name'.

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 \<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