--- a/Nominal/Ex/Datatypes.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/Datatypes.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -8,7 +8,7 @@
   atom_decl - example by John Matthews
 *)
 
-nominal_datatype 'a Maybe = 
+nominal_datatype 'a::fs Maybe = 
   Nothing 
 | Just 'a
 

--- a/Nominal/Ex/Finite_Alpha.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/Finite_Alpha.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -8,7 +8,12 @@
       and "p \<bullet> as = bs"
     shows "(as, x) \<approx>set (op =) supp p (bs, y)"
   using assms unfolding alphas
-  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt)
+  apply(simp)
+  apply(clarify)
+  apply(simp only: Diff_eqvt[symmetric] supp_eqvt[symmetric])
+  apply(simp only: atom_set_perm_eq)
+  done
+
 
 lemma
   assumes "(supp x - set as) \<sharp>* p"
@@ -16,7 +21,11 @@
       and "p \<bullet> as = bs"
     shows "(as, x) \<approx>lst (op =) supp p (bs, y)"
   using assms unfolding alphas
-  by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list)
+  apply(simp)
+  apply(clarify)
+  apply(simp only: set_eqvt[symmetric] Diff_eqvt[symmetric] supp_eqvt[symmetric])
+  apply(simp only: atom_set_perm_eq)
+  done
 
 lemma
   assumes "(supp x - as) \<sharp>* p"
@@ -32,8 +41,8 @@
   apply (rule trans)
   apply (rule supp_perm_eq[symmetric, of _ p])
   apply (simp add: supp_finite_atom_set fresh_star_def)
-  apply blast
-  apply (simp add: eqvts)
+  apply(auto)[1]
+  apply(simp only: Diff_eqvt inter_eqvt supp_eqvt)
   apply (simp add: fresh_star_def)
   apply blast
   done

--- a/Nominal/Ex/Lambda.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -169,7 +169,7 @@
 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])"
   apply(simp add: eqvt_def subst'_graph_def)
-  apply (rule, perm_simp, rule)
+  apply(perm_simp, simp)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)

--- a/Nominal/Ex/LetRec2.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/LetRec2.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -22,6 +22,11 @@
 thm trm_assn.eq_iff
 thm trm_assn.supp
 
+ML {*
+@{term Trueprop} ;
+@{const_name HOL.eq}
+*}
+
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff
 thm trm_assn.bn_defs

--- a/Nominal/Ex/TypeVarsTest.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -17,9 +17,9 @@
 instance nat :: s1 ..
 instance int :: s2 .. 
 
-nominal_datatype ('a, 'b, 'c) lam =
+nominal_datatype ('a::"{s1,fs}", 'b::"{s2,fs}", 'c::at) lam =
   Var "name"
-| App "('a::s1, 'b::s2, 'c::at) lam" "('a, 'b, 'c) lam"
+| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
 | Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
 | Foo "'a" "'b"
 | Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
@@ -41,11 +41,11 @@
 
 nominal_datatype ('alpha, 'beta, 'gamma) psi =
   PsiNil
-| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
+| Output "'alpha::fs" "'alpha::fs" "('alpha::fs, 'beta::fs, 'gamma::fs) psi" 
 
 
 nominal_datatype 'a foo = 
-  Node x::"name" f::"'a foo" binds x in f
+  Node x::"name" f::"('a::fs) foo" binds x in f
 | Leaf "'a"
 
 term "Leaf"

--- a/Nominal/Nominal2.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -60,10 +60,10 @@
 
 ML {*
 fun get_cnstrs dts =
-  map (fn (_, _, _, constrs) => constrs) dts
+  map snd dts
 
 fun get_typed_cnstrs dts =
-  flat (map (fn (_, bn, _, constrs) => 
+  flat (map (fn ((bn, _, _), constrs) => 
    (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
 
 fun get_cnstr_strs dts =
@@ -94,8 +94,8 @@
   fun raw_dts_aux1 (bind, tys, _) =
     (raw_bind bind, map (replace_typ ty_ss) tys, NoSyn)
 
-  fun raw_dts_aux2 (ty_args, bind, _, constrs) =
-    (ty_args, raw_bind bind, NoSyn, map raw_dts_aux1 constrs)
+  fun raw_dts_aux2 ((bind, ty_args, _), constrs) =
+    ((raw_bind bind, ty_args, NoSyn), map raw_dts_aux1 constrs)
 in
   map raw_dts_aux2 dts
 end
@@ -146,7 +146,7 @@
   val thy = Local_Theory.exit_global lthy
   val thy_name = Context.theory_name thy
 
-  val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+  val dt_names = map (fn ((s, _, _), _) => Binding.name_of s) dts
   val dt_full_names = map (Long_Name.qualify thy_name) dt_names 
   val dt_full_names' = add_raws dt_full_names
   val dts_env = dt_full_names ~~ dt_full_names'
@@ -333,7 +333,7 @@
       alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
 
   val _ = trace_msg (K "Defining the quotient types...")
-  val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
+  val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
     let
@@ -527,45 +527,58 @@
 
 section {* Preparing and parsing of the specification *}
 
+ML {*
+fun parse_spec ctxt ((tname, tvs, mx), constrs) =
+let
+  val tvs' = map (apsnd (Typedecl.read_constraint ctxt)) tvs
+  val constrs' = constrs
+    |> map (fn (c, Ts, mx', bns) => (c, map ((Syntax.parse_typ ctxt) o snd) Ts, mx'))
+in
+  ((tname, tvs', mx), constrs')
+end
+
+fun check_specs ctxt specs =
+  let
+    fun prep_spec ((tname, args, mx), constrs) tys =
+      let
+        val (args', tys1) = chop (length args) tys;
+        val (constrs', tys3) = (constrs, tys1) |-> fold_map (fn (cname, cargs, mx') => fn tys2 =>
+          let val (cargs', tys3) = chop (length cargs) tys2;
+          in ((cname, cargs', mx'), tys3) end);
+      in 
+        (((tname, map dest_TFree args', mx), constrs'), tys3) 
+      end
+
+    val all_tys =
+      specs |> maps (fn ((_, args, _), cs) => map TFree args @ maps #2 cs)
+      |> Syntax.check_typs ctxt;
+
+  in 
+    #1 (fold_map prep_spec specs all_tys) 
+  end
+*}
+
 ML {* 
 (* generates the parsed datatypes and 
    declares the constructors 
 *)
 fun prepare_dts dt_strs thy = 
 let
-  fun inter_fs_sort thy (a, S) = 
-    (a, Type.inter_sort (Sign.tsig_of thy) (@{sort fs}, S)) 
-
-  fun mk_type tname sorts (cname, cargs, mx) =
-  let
-    val full_tname = Sign.full_name thy tname
-    val ty = Type (full_tname, map (TFree o inter_fs_sort thy) sorts)
-  in
-    (cname, cargs ---> ty, mx)
-  end
+  val ctxt = Proof_Context.init_global thy
+    |> fold (fn ((_, args, _), _) => fold (fn (a, _) =>
+         Variable.declare_typ (TFree (a, dummyS))) args) dt_strs
+ 
+  val dts = check_specs ctxt (map (parse_spec ctxt) dt_strs)
+  
+  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 
 
-  fun prep_constr (cname, cargs, mx, _) (constrs, sorts) =
-  let 
-    val (cargs', sorts') = 
-      fold_map (Datatype.read_typ thy) (map snd cargs) sorts
-      |>> map (map_type_tfree (TFree o inter_fs_sort thy)) 
-  in 
-    (constrs @ [(cname, cargs', mx)], sorts') 
-  end
-  
-  fun prep_dts (tvs, tname, mx, constrs) (constr_trms, dts, sorts) =
-  let 
-
-    val (constrs', sorts') = 
-      fold prep_constr constrs ([], sorts)
-
-    val constr_trms' = 
-      map (mk_type tname (rev sorts')) constrs'
-  in 
-    (constr_trms @ constr_trms', dts @ [(tvs, tname, mx, constrs')], sorts') 
-  end
-
-  val (constr_trms, dts, sorts) = fold prep_dts dt_strs ([], [], []);
+  val constr_trms = flat (map mk_constr_trms dts)
 in
   thy
   |> Sign.add_consts_i constr_trms
@@ -681,7 +694,7 @@
 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
 let
   val pre_typs = 
-    map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dt_strs
+    map (fn ((tname, tvs, mx), _) => (tname, length tvs, mx)) dt_strs
 
   (* this theory is used just for parsing *)
   val thy = Proof_Context.theory_of lthy  
@@ -707,6 +720,7 @@
   structure S = Scan
 
   fun triple ((x, y), z) = (x, y, z)
+  fun triple2 ((x, y), z) = (y, x, z)
   fun tuple1 ((x, y, z), u) = (x, y, z, u)
   fun tuple2 (((x, y), z), u) = (x, y, u, z)
   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
@@ -730,8 +744,8 @@
 
 (* datatype parser *)
 val dt_parser =
-  (P.type_args -- P.binding -- P.opt_mixfix >> triple) -- 
-    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple1
+  (P.type_args_constrained -- P.binding -- P.opt_mixfix >> triple2) -- 
+    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser)
 
 (* binding function parser *)
 val bnfun_parser = 
@@ -748,11 +762,6 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-(*
-ML {*
-trace := true
-*}
-*)
 
 end
 

--- a/Nominal/Nominal2_Base.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -2312,6 +2312,9 @@
   qed
 qed
 
+
+
+
 lemma supp_perm_perm_eq:
   assumes a: "\<forall>a \<in> supp x. p \<bullet> a = q \<bullet> a"
   shows "p \<bullet> x = q \<bullet> x"

--- a/Nominal/nominal_dt_data.ML	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/nominal_dt_data.ML	Thu Dec 15 16:20:42 2011 +0000
@@ -5,9 +5,6 @@
 
 signature NOMINAL_DT_DATA =
 sig
-  (* info of raw datatypes *)
-  type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
-
   (* info of raw binding functions *)
   type bn_info = term * int * (int * term option) list list
 
@@ -28,7 +25,7 @@
   val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
 
   datatype user_data = UserData of
-    {dts      : dt_info,
+    {dts      : Datatype.spec list,
      cn_names : string list,
      cn_tys   : (string * string) list,
      bn_funs  : (binding * typ * mixfix) list,
@@ -37,7 +34,7 @@
 
   datatype raw_dt_info = RawDtInfo of
     {raw_dt_names         : string list,
-     raw_dts              : dt_info,
+     raw_dts              : Datatype.spec list,
      raw_tys              : typ list,
      raw_ty_args          : (string * sort) list,
      raw_cns_info         : cns_info list,
@@ -66,13 +63,6 @@
 structure Nominal_Dt_Data: NOMINAL_DT_DATA =
 struct
 
-(* string list      - type variables of a datatype
-   binding          - name of the datatype
-   mixfix           - its mixfix
-   (binding * typ list * mixfix) list  - datatype constructors of the type
-*)  
-type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
-
 
 (* term              - is constant of the bn-function 
    int               - is datatype number over which the bn-function is defined
@@ -121,7 +111,7 @@
 
 
 datatype user_data = UserData of
-  {dts      : dt_info,
+  {dts      : Datatype.spec list,
    cn_names : string list,
    cn_tys   : (string * string) list,
    bn_funs  : (binding * typ * mixfix) list,
@@ -130,7 +120,7 @@
 
 datatype raw_dt_info = RawDtInfo of
   {raw_dt_names         : string list,
-   raw_dts              : dt_info,
+   raw_dts              : Datatype.spec list,
    raw_tys              : typ list,
    raw_ty_args          : (string * sort) list,
    raw_cns_info         : cns_info list,

--- a/Nominal/nominal_dt_rawfuns.ML	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Dec 15 16:20:42 2011 +0000
@@ -94,7 +94,7 @@
   fun cntrs_order ((bn, dt_index), data) = 
   let
     val dt = nth dts dt_index                      
-    val cts = (fn (_, _, _, x) => x) dt     
+    val cts = snd dt     
     val ct_names = map (Binding.name_of o (fn (x, _, _) => x)) cts  
   in
     (bn, (bn, dt_index, order (op=) ct_names data))