# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267537900 -3600
# Node ID dc65319809cc460b4204f71b9493aaf91194ec47
# Parent  c28403308b3471c6ae19d02c3eb4c440cecc88ba
Change type schemes to name set.

diff -r c28403308b34 -r dc65319809cc Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 14:24:57 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 14:51:40 2010 +0100
@@ -68,22 +68,20 @@
 
 text {* example type schemes *}
 
+(* does not work yet
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
 
-(* does not work yet
 nominal_datatype tyS =
   All xs::"name list" ty::"t_raw" bind xs in ty
 *)
 
-(* also does not work
 nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 and  tyS = 
-  All xs::"name list" ty::"t" bind xs in ty
-*)
+  All xs::"name set" ty::"t" bind xs in ty
 
 (* example 1 from Terms.thy *)