# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264596245 -3600
# Node ID 8a16d6c45720d041f41c46f74e662f4a814fee7c
# Parent  0f88e04eb486142733bba1cf7b5813db41d90e94
Another string in the specification.

diff -r 0f88e04eb486 -r 8a16d6c45720 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Jan 27 13:32:28 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 13:44:05 2010 +0100
@@ -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