--- a/Nominal/Parser.thy	Mon Mar 01 16:04:03 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 16:55:41 2010 +0100
@@ -88,10 +88,9 @@
 
 fun raw_dts ty_ss dts =
 let
-  val ty_ss' = ty_ss ~~ (add_raws ty_ss)
 
   fun raw_dts_aux1 (bind, tys, mx) =
-    (raw_bind bind, map (replace_typ ty_ss') tys, mx)
+    (raw_bind bind, map (replace_typ ty_ss) tys, mx)
 
   fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
     (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
@@ -108,26 +107,24 @@
 *}
 
 ML {*
-fun get_constrs dts =
+fun get_cnstrs dts =
   flat (map (fn (_, _, _, constrs) => constrs) dts)
 
-fun get_typed_constrs dts =
+fun get_typed_cnstrs dts =
   flat (map (fn (_, bn, _, constrs) => 
    (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
 
-fun get_constr_strs dts =
-  map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts)
+fun get_cnstr_strs dts =
+  map (fn (bn, _, _) => Binding.name_of bn) (get_cnstrs dts)
 
 fun get_bn_fun_strs bn_funs =
   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 *}
 
 ML {*
-fun raw_dts_decl dt_names dts lthy =
+fun rawify_dts dt_names dts dts_env =
 let
-  val thy = ProofContext.theory_of lthy
-  val dt_full_names = map (Sign.full_bname thy) dt_names 
-  val raw_dts = raw_dts dt_full_names dts
+  val raw_dts = raw_dts dts_env dts
   val raw_dt_names = add_raws dt_names
 in
   (raw_dt_names, raw_dts)
@@ -135,52 +132,65 @@
 *}
 
 ML {*
-fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
+fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
+let
+  val bn_funs' = map (fn (bn, ty, mx) => 
+    (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
+  
+  val bn_eqs' = map (fn (attr, trm) => 
+    (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+in
+  (bn_funs', bn_eqs') 
+end 
+*}
+
+ML {* 
+fun add_primrec_wrapper funs eqs lthy = 
+  if null funs then (([], []), lthy)
+  else 
+   let 
+     val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
+     val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
+   in 
+     Primrec.add_primrec funs' eqs' lthy
+   end
+*}
+
+
+ML {* 
+fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
   val thy = ProofContext.theory_of lthy
+  val thy_name = Context.theory_name thy
+  
+  val conf = Datatype.default_config
 
-  val dt_names' = add_raws dt_names
-  val dt_full_names = map (Sign.full_bname thy) dt_names 
-  val dt_full_names' = map (Sign.full_bname thy) dt_names' 
-  val dt_env = dt_full_names ~~ dt_full_names'
-  
-  val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts)
-  val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y))) 
-    (get_typed_constrs dts)
-  val ctrs_env = ctrs_names ~~ ctrs_names'
+  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'
+
+  val cnstrs = get_cnstr_strs dts
+  val cnstrs_ty = get_typed_cnstrs dts
+  val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
+  val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name 
+    (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
+  val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
 
   val bn_fun_strs = get_bn_fun_strs bn_funs
   val bn_fun_strs' = add_raws bn_fun_strs
   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-  
-  val bn_funs' = map (fn (bn, ty, mx) => 
-    (raw_bind bn, SOME (replace_typ dt_env ty), mx)) bn_funs
-  
-  val bn_eqs' = map (fn (_, trm) => 
-    (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
-in
-  if null bn_eqs 
-  then (([], []), lthy)
-  else Primrec.add_primrec bn_funs' bn_eqs' lthy 
-end 
-*}
+
+  val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
 
-ML {* 
-fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
-let
-  val conf = Datatype.default_config
-  val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
-
-  val (raw_dt_names, raw_dts) = raw_dts_decl dts_names dts lthy
-
+  val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
 in
-  lthy
-  |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
-  ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
+  lthy 
+  |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts) 
+  ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
 end
 *}
 
-
 ML {* 
 (* parsing the datatypes and declaring *)
 (* constructors in the local theory    *)
@@ -307,7 +317,7 @@
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
     ||> prepare_binds dt_strs
   
-  val _ = tracing (PolyML.makestring binds)
+  (*val _ = tracing (PolyML.makestring binds)*)
 in
   nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
 end