diff -r 31d51ce547b7 -r 2b1b8404fe0d Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Dec 17 20:03:37 2011 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 18 00:42:32 2011 +0000
@@ -526,63 +526,35 @@
 
 
 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
-  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 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
+      map (fn (c, tys, mx) => (c, (tys ---> ty), mx)) constrs
     end 
 
+  val (dts, spec_ctxt) = 
+    Datatype.read_specs (map prep_spec dt_strs) thy
+ 
   val constr_trms = flat (map mk_constr_trms dts)
+ 
+  (* 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
-  thy
-  |> Sign.add_consts_i constr_trms
-  |> pair dts
+  (dts, thy')
 end
 *}
 
@@ -599,6 +571,7 @@
   fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
   
   val bn_funs' = map prep_bn_fun bn_funs
+
 in
   (Local_Theory.exit_global lthy')
   |> Sign.add_consts_i bn_funs'
@@ -693,23 +666,18 @@
 ML {*
 fun nominal_datatype2_cmd (opt_thms_name, dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
 let
-  val pre_typs = 
-    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  
-  val tmp_thy = Theory.copy thy 
 
-  val (((dts, (bn_funs, bn_eqs)), bclauses), tmp_thy') = 
-    tmp_thy
-    |> Sign.add_types_global pre_typs
+  val (((dts, (bn_funs, bn_eqs)), bclauses), thy') = 
+    thy
     |> prepare_dts dt_strs 
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 
-    ||>> prepare_bclauses dt_strs 
+    ||>> prepare_bclauses dt_strs
 
   val bclauses' = complete dt_strs bclauses
 in
-  nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy
+  nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses' lthy 
 end
 *}
 
@@ -719,9 +687,8 @@
   structure P = Parse;
   structure S = Scan
 
-  fun triple ((x, y), z) = (x, y, z)
+  fun triple1 ((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)
 in
@@ -737,7 +704,7 @@
     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
 
 val bind_clauses = 
-  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
+  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
 
 val cnstr_parser =
   P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tuple2