diff -r 24889782da92 -r 2d17ed8aca60 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Mon Mar 01 21:50:24 2010 +0100
+++ b/Nominal/Parser.thy	Mon Mar 01 21:50:40 2010 +0100
@@ -4,7 +4,6 @@
 
 atom_decl name
 
-
 section{* Interface for nominal_datatype *}
 
 text {*
@@ -88,10 +87,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 +106,24 @@
 *}
 
 ML {*
-fun get_constrs dts =
-  flat (map (fn (_, _, _, constrs) => constrs) dts)
+fun get_cnstrs dts =
+  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) (flat (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 +131,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    *)
@@ -236,14 +245,12 @@
 *}
 
 ML {*
-fun forth (_, _, _, x) = x
-
-fun find_all eq xs k' = 
-  maps (fn (k, v) => if eq (k, k') then [v] else []) xs
+fun find_all eq xs (k',i) = 
+  maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs
 *}
 
 ML {*
-(* associates every SOME with the index in the list *)
+(* associates every SOME with the index in the list; drops NONEs *)
 fun mk_env xs =
   let
     fun mapp (_: int) [] = []
@@ -261,37 +268,35 @@
   | NONE => error ("cannot find " ^ x ^ " in the binding specification.");
 *}
 
-
-
 ML {*
 fun prepare_binds dt_strs lthy = 
 let
   fun extract_annos_binds dt_strs =
-    map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
+    map (map (fn (_, antys, _, bns) => (map fst antys, bns))) 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)))
+       Free (x, _) => (NONE, env_lookup env x)
+     | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x)
      | _ => error (bn_str ^ " not allowed as binding specification.");  
  
-  fun prep_typ env opt_name = 
+  fun prep_typ env (i, opt_name) = 
     case opt_name of
       NONE => []
-    | SOME x => find_all (op=) env x;
+    | SOME x => find_all (op=) env (x,i);
         
   (* annos - list of annotation for each type (either NONE or SOME fo a type *)
   
   fun prep_binds (annos, bind_strs) = 
   let
-    val env = mk_env annos (* for ever label the index *)
+    val env = mk_env annos (* for every label the index *)
     val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs  
   in
-    map (prep_typ binds) annos
+    map_index (prep_typ binds) annos
   end
 
 in
-  map (map prep_binds) (extract_annos_binds dt_strs)
+  map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))
 end
 *}