--- a/Nominal/NewParser.thy	Mon Jun 28 15:23:56 2010 +0100
+++ b/Nominal/NewParser.thy	Mon Jun 28 16:22:28 2010 +0100
@@ -425,8 +425,8 @@
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
-  val qty_binds = map (fn (_, bind, _, _) => bind) dts            (* not used *)
-  val qty_names = map Name.of_binding qty_binds;                  (* not used *)
+  val qty_binds = map (fn (_, bind, _, _) => bind) dts        
+  val qty_names = map Name.of_binding qty_binds;              
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
   
   val (qty_infos, lthy7) = 
@@ -435,21 +435,28 @@
     else raise TEST lthy6
 
   val qtys = map #qtyp qty_infos
-  val qconstr_descrs = 
+  
+  (* defining of quotient term-constructors, binding functions, free vars functions *)
+  val qconstr_descr = 
     flat (map (fn (_, _, _, cs) => map (fn (b, _, mx) => (Name.of_binding b, mx)) cs) dts)
     |> map2 (fn t => fn (b, mx) => (b, t, mx)) all_raw_constrs
 
-  val (qconstrs, lthy8) = 
+  val qbns_descr =
+    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs
+
+  val qfvs_descr = 
+    map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs
+
+
+  val (qs, lthy8) = 
     if get_STEPS lthy > 15
-    then qconst_defs qtys qconstr_descrs lthy7
+    then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7
     else raise TEST lthy7
 
+  val _ = tracing ("raw fvs  " ^ commas (map @{make_string} raw_fvs))
+  val _ = tracing ("raw fv_bns  " ^ commas (map @{make_string} raw_fv_bns))
+
   (* HERE *)
-
-  val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys))
-  val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs))
-  val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys))
-  val _ = tracing ("qconstrs " ^ commas (map @{make_string} qconstrs))
   
   val _ = 
     if get_STEPS lthy > 16
@@ -498,7 +505,7 @@
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ alpha_refl_thms @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
-    val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
+  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;