--- a/Nominal/Ex/TypeVarsTest.thy	Thu Dec 22 04:35:01 2011 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Dec 22 13:10:30 2011 +0000
@@ -17,7 +17,7 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam =
+nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
   Var "name"
 | App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
 | Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
@@ -41,11 +41,11 @@
 
 nominal_datatype ('alpha, 'beta, 'gamma) psi =
   PsiNil
-| Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" 
+| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
 nominal_datatype 'a foo = 
-  Node x::"name" f::"('a::fs) foo" binds x in f
+  Node x::"name" f::"'a foo" binds x in f
 | Leaf "'a"
 
 term "Leaf"

--- a/Nominal/Nominal2.thy	Thu Dec 22 04:35:01 2011 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 22 13:10:30 2011 +0000
@@ -526,41 +526,54 @@
 
 
 section {* Preparing and parsing of the specification *}
+
+ML {*
+(* adds the default sort @{sort fs} to nominal specifications *)
+
+fun augment_sort thy S = Sign.inter_sort thy (@{sort fs}, S)
+
+fun augment_sort_typ thy =
+  map_type_tfree (fn (s, S) => TFree (s, augment_sort thy S))
+*}
+
 ML {* 
-(* generates the parsed datatypes and 
-   declares the constructors 
-*)
+(* generates the parsed datatypes and declares the constructors *)
 
 fun prepare_dts dt_strs thy = 
 let
   fun prep_spec ((tname, tvs, mx), constrs) =
-    ((tname, tvs, mx), 
-      constrs |> map (fn (c, Ts, mx', _) => (c, map snd Ts, mx')))
-
-  fun mk_constr_trms ((tname, tvs, _), constrs) =
-    let
-      val full_tname = Sign.full_name thy tname
-      val ty = Type (full_tname, map TFree tvs)
-    in
-      map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
-    end 
+    ((tname, tvs, mx), constrs |> map (fn (c, atys, mx', _) => (c, map snd atys, mx')))
 
   val (dts, spec_ctxt) = 
     Datatype.read_specs (map prep_spec dt_strs) thy
  
-  val constr_trms = flat (map mk_constr_trms dts)
- 
+  fun augment ((tname, tvs, mx), constrs) =
+    ((tname, map (apsnd (augment_sort thy)) tvs, mx), 
+      constrs |> map (fn (c, tys, mx') => (c, map (augment_sort_typ thy) tys, mx')))
+  
+  val dts' = map augment dts
+
+  fun mk_constr_trms ((tname, tvs, _), constrs) =
+    let
+      val ty = Type (Sign.full_name thy tname, map TFree tvs)
+    in
+      map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
+    end
+
+  val constr_trms = flat (map mk_constr_trms dts')
+  
+  (* FIXME: local version *)
   (* val (_, spec_ctxt') = Proof_Context.add_fixes constr_trms spec_ctxt *)
+
   val thy' = Sign.add_consts_i constr_trms (Proof_Context.theory_of spec_ctxt)
-
 in
-  (dts, thy')
+  (dts', thy')
 end
 *}
 
 ML {*
-(* parsing the binding function specification and *)
-(* declaring the functions in the local theory    *)
+(* parsing the binding function specifications and *)
+(* declaring the function constants                *)
 fun prepare_bn_funs bn_fun_strs bn_eq_strs thy =
 let
   val lthy = Named_Target.theory_init thy
@@ -669,7 +682,7 @@
   (* this theory is used just for parsing *)
   val thy = Proof_Context.theory_of lthy  
 
-  val (((dts, (bn_funs, bn_eqs)), bclauses), thy') = 
+  val (((dts, (bn_funs, bn_eqs)), bclauses), _) = 
     thy
     |> prepare_dts dt_strs 
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs