--- a/Nominal/Parser.thy	Sat Feb 27 11:54:59 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 07:46:50 2010 +0100
@@ -217,8 +217,8 @@
 *}
 
 ML {*
-(* parsing the function specification and *)
-(* declaring the functions in the local theory *)
+(* parsing the binding function specification and *)
+(* declaring the functions in the local theory    *)
 fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
 let
   fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
@@ -237,21 +237,22 @@
 ML {*
 fun forth (_, _, _, x) = x
 
-fun find_all eq [] _ = []
-  | find_all eq ((key, value)::xs) key' = 
-      let
-        val values = find_all eq xs key'
-      in if eq (key', key) then value :: values else values end;
+fun find_all eq xs k' = 
+  maps (fn (k, v) => if eq (k, k') then [v] else []) xs
+*}
 
+ML {*
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
-      | mapp i ((a, _) :: xs) = 
+      | mapp i (a :: xs) = 
          case a of
            NONE => mapp (i + 1) xs
          | SOME x => (x, i) :: mapp (i + 1) xs
   in mapp 0 xs end
+*}
 
+ML {*
 fun env_lookup xs x =
   case AList.lookup (op =) xs x of
     SOME x => x
@@ -261,34 +262,35 @@
 ML {*
 fun prepare_binds dt_strs lthy = 
 let
-  fun prep_bn env str =
-        (case Syntax.read_term lthy str of
-           Free (x, _) => (env_lookup env x, NONE)
-         | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
-         | x => error (str ^ " not allowed as binding specification."))   
+  fun extract_cnstrs dt_strs =
+    map ((map (fn (_, antys, _, bns) => (antys, bns))) o forth) dt_strs
+
+  fun prep_bn env bn_str =
+    case (Syntax.read_term lthy bn_str) of
+       Free (x, _) => (env_lookup env x, NONE)
+     | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
+     | _ => error (bn_str ^ " not allowed as binding specification.");  
  
   fun prep_typ env (opt_name, _) = 
-        (case opt_name of
-           NONE => []
-         | SOME x => find_all (op=) env x)
+    case opt_name of
+      NONE => []
+    | SOME x => find_all (op=) env x;
         
-  fun prep_binds (_, anno_tys, _, bind_strs) = 
+  fun prep_binds (anno_tys, bind_strs) = 
   let
-    val env = mk_env anno_tys
+    val env = mk_env (map fst anno_tys)
     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   in
     map (prep_typ binds) anno_tys
   end
 in
-  map ((map prep_binds) o forth) dt_strs
+  map (map prep_binds) (extract_cnstrs dt_strs)
 end
 *}
 
 ML {*
 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
 let
-  val t = start_timing ()
-
   fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
 
   val ((dts, (bn_fun, bn_eq)), binds) = 
@@ -299,7 +301,6 @@
     ||> prepare_binds dt_strs
   
   val _ = tracing (PolyML.makestring binds)
-  val _ = tracing (#message (end_timing t))
 in
   nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
 end

--- a/Nominal/Test.thy	Sat Feb 27 11:54:59 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 01 07:46:50 2010 +0100
@@ -63,6 +63,7 @@
 thm f0_raw.simps
 
 text {* example type schemes *}
+
 datatype t = 
   Var "name" 
 | Fun "t" "t"
@@ -197,8 +198,20 @@
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
 
-(* example form Leroy 96 about modules *)
+(* example from my PHD *)
+
+atom_decl coname
 
+nominal_datatype phd =
+   Ax name coname
+|  Cut n::name t1::phd c::coname t2::phd               bind n in t1, bind c in t2
+|  AndR c1::coname t1::phd c2::coname t2::phd coname   bind c1 in t1, bind c2 in t2
+|  AndL1 n::name t::phd name                           bind n in t
+|  AndL2 n::name t::phd name                           bind n in t
+|  ImpL c::coname t1::phd n::name t2::phd name         bind c in t1, bind n in t2
+|  ImpR c::coname n::name t::phd coname                bind n in 1, bind c in t
+
+(* example form Leroy 96 about modules; OTT *)
 
 nominal_datatype mexp =
   Acc path