--- a/Nominal/NewParser.thy	Wed May 19 12:44:03 2010 +0100
+++ b/Nominal/NewParser.thy	Thu May 20 21:23:53 2010 +0100
@@ -2,9 +2,10 @@
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Nominal2_Supp" 
-        "Perm" "NewFv" "NewAlpha" "Tacs" "Equivp" "Lift"
+        "Perm" "NewAlpha" "Tacs" "Equivp" "Lift"
 begin
 
+
 section{* Interface for nominal_datatype *}
 
 
@@ -154,10 +155,7 @@
   fun rawify_bnds bnds = 
     map (apfst (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env))) bnds
 
-  fun rawify_bclause (BEmy n) = BEmy n
-    | rawify_bclause (BLst (bnds, bdys)) = BLst (rawify_bnds bnds, bdys)
-    | rawify_bclause (BSet (bnds, bdys)) = BSet (rawify_bnds bnds, bdys)
-    | rawify_bclause (BRes (bnds, bdys)) = BRes (rawify_bnds bnds, bdys)
+  fun rawify_bclause (BC (mode, bnds, bdys)) = BC (mode, rawify_bnds bnds, bdys)
 in
   map (map (map rawify_bclause)) bclauses
 end
@@ -219,9 +217,9 @@
   val ordered = map (fn (x, y) => (x, map (fn (v, z) => (v, order dts x z)) y)) unordered' 
   val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 
-  val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
+  (*val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))*)
   (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
-  val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
+  (*val _ = tracing ("ordered'\n" ^ @{make_string} ordered')*)
 in
   ordered'
 end
@@ -263,7 +261,7 @@
   fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
   val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
 in
-  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2)
+  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, raw_bns, lthy2)
 end
 *}
 
@@ -372,10 +370,13 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes and raw bn-functions *)
-  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
+  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, raw_bns2, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  (*val _ = tracing ("exported: " ^ commas (map @{make_string} raw_bns))*)
+  (*val _ = tracing ("plain: " ^ commas (map @{make_string} raw_bns2))*)
+
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
   val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
@@ -408,7 +409,7 @@
 
   val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs descr sorts raw_bns raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bns raw_bns2 raw_bclauses lthy3
     else raise TEST lthy3
   
   (* definition of raw alphas *)
@@ -431,7 +432,8 @@
   (* definition of raw_alpha_eq_iff  lemmas *)
   val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
   val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
-  val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+  
+  (*val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);*)
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
@@ -639,16 +641,16 @@
  
   fun prep_body env bn_str = index_lookup env bn_str
 
-  fun prep_mode "bind"     = BLst 
-    | prep_mode "bind_set" = BSet 
-    | prep_mode "bind_res" = BRes 
+  fun prep_mode "bind"     = Lst 
+    | prep_mode "bind_set" = Set 
+    | prep_mode "bind_res" = Res 
 
   fun prep_bclause env (mode, binders, bodies) = 
   let
     val binders' = map (prep_binder env) binders
     val bodies' = map (prep_body env) bodies
   in  
-    prep_mode mode (binders', bodies')
+    BC (prep_mode mode, binders', bodies')
   end
 
   fun prep_bclauses (annos, bclause_strs) = 
@@ -670,10 +672,7 @@
 ML {*
 fun included i bcs = 
 let
-  fun incl (BEmy j) = i = j
-    | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
-    | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
-    | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
+  fun incl (BC (_, bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
 in
   exists incl bcs 
 end
@@ -688,7 +687,7 @@
 
   fun complt n bcs = 
   let
-    fun add bcs i = (if included i bcs then [] else [BEmy i]) 
+    fun add bcs i = (if included i bcs then [] else [BC (Lst, [], [i])]) 
   in
     bcs @ (flat (map_range (add bcs) n))
   end