--- a/Nominal/NewParser.thy	Fri Jul 02 15:34:46 2010 +0100
+++ b/Nominal/NewParser.thy	Wed Jul 07 09:34:00 2010 +0100
@@ -336,7 +336,7 @@
   val _ = warning "Definition of raw fv-functions";
   val lthy3 = Theory_Target.init NONE thy;
 
-  val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
+  val (raw_bns, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
     if get_STEPS lthy3 > 2 
     then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
     else raise TEST lthy3
@@ -370,7 +370,7 @@
   val _ = warning "Proving equivariance";
   val bn_eqvt = 
     if get_STEPS lthy > 6
-    then raw_prove_eqvt raw_bn_funs raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
+    then raw_prove_eqvt raw_bns raw_bn_induct (raw_bn_eqs @ raw_perm_defs) lthy4
     else raise TEST lthy4
 
   (* noting the bn_eqvt lemmas in a temprorary theory *)
@@ -437,25 +437,38 @@
   val qtys = map #qtyp qty_infos
   
   (* defining of quotient term-constructors, binding functions, free vars functions *)
-  val qconstr_descr = 
+  val _ = warning "Defining the quotient constnats"
+  val qconstrs_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 qbns_descr =
-    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bn_funs
+    map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
 
   val qfvs_descr = 
-    map2 (fn n => fn t => (n, t, NoSyn)) qty_names raw_fvs
+    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn)) qty_names raw_fvs
 
+  val qfv_bns_descr = 
+    map2 (fn (b, _, _) => fn t => ("fv_" ^ Name.of_binding b, t, NoSyn)) bn_funs  raw_fv_bns
 
-  val (qs, lthy8) = 
+  (* TODO: probably also needs alpha_bn *)
+  val ((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), lthy8) = 
     if get_STEPS lthy > 15
-    then qconst_defs qtys (qconstr_descr @ qbns_descr @ qfvs_descr) lthy7
+    then 
+      lthy7
+      |> qconst_defs qtys qconstrs_descr 
+      ||>> qconst_defs qtys qbns_descr 
+      ||>> qconst_defs qtys qfvs_descr
+      ||>> qconst_defs qtys qfv_bns_descr
     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))
+  val qconstrs = map #qconst qconstrs_info
+  val qbns = map #qconst qbns_info
+  val qfvs = map #qconst qfvs_info
+  val qfv_bns = map #qconst qfv_bns_info
 
+  (* respectfulness proofs *)
+  
   (* HERE *)
   
   val _ = 
@@ -464,18 +477,10 @@
   
   (* old stuff *)
 
-  val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
-  val raw_consts =
-    flat (map (fn (i, (_, _, l)) =>
-      map (fn (cname, dts) =>
-        Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
-          Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts
-  val (consts, _, lthy8) = quotient_lift_consts_export qtys dd lthy7;
   val _ = warning "Proving respects";
 
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
+  val bns = raw_bns ~~ bn_nos;
 
   val bns_rsp_pre' = build_fvbv_rsps alpha_trms alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
@@ -504,27 +509,36 @@
     let val alpha_alphabn = prove_alpha_alphabn alpha_trms alpha_induct alpha_eq_iff alpha_bn_trms lthy11a
       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
+    const_rsp_tac) all_raw_constrs lthy11a
   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_info, lthy12a) = qconst_defs qtys dd lthy12;
+  val qfv_ts = map #qconst qfv_info
+  val qfv_defs = map #def qfv_info
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
-  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs
-  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a;
+  val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bns
+  val (qbn_info, lthy12b) = qconst_defs qtys dd lthy12a;
+  val qbn_ts = map #qconst qbn_info
+  val qbn_defs = map #def qbn_info
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
-  val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b;
+  val (qalpha_info, lthy12c) = qconst_defs qtys dd lthy12b;
+  val qalpha_bn_trms = map #qconst qalpha_info
+  val qalphabn_defs = map #def qalpha_info
+  
   val _ = warning "Lifting permutations";
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
-  val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy;
+  (* use Local_Theory.theory_result *)
+  val thy' = qperm_defs qtys qty_full_names dd raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
+  
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
-  val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
+  val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs;
   val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
@@ -556,7 +570,7 @@
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = warning "Supports";
-  val supports = map (prove_supports lthy20 q_perm) consts;
+  val supports = map (prove_supports lthy20 q_perm) qconstrs;
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val _ = warning "Instantiating FS";