diff -r aecebd5ed424 -r 72ad4e766acf Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri May 21 11:40:18 2010 +0100
+++ b/Nominal/NewParser.thy	Sat May 22 13:51:47 2010 +0100
@@ -165,18 +165,23 @@
    appends of elements; in case of recursive calls it retruns also the applied
    bn function *)
 ML {*
-fun strip_bn_fun t =
-  case t of
-    Const (@{const_name sup}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
-  | Const (@{const_name append}, _) $ l $ r => strip_bn_fun l @ strip_bn_fun r
-  | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
-      (i, NONE) :: strip_bn_fun y
-  | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ Bound i) $ y =>
-      (i, NONE) :: strip_bn_fun y
-  | Const (@{const_name bot}, _) => []
-  | Const (@{const_name Nil}, _) => []
-  | (f as Free _) $ Bound i => [(i, SOME f)]
-  | _ => error ("Unsupported binding function: " ^ (PolyML.makestring t))
+fun strip_bn_fun lthy args t =
+let 
+  fun aux t =
+    case t of
+      Const (@{const_name sup}, _) $ l $ r => aux l @ aux r
+    | Const (@{const_name append}, _) $ l $ r => aux l @ aux r
+    | Const (@{const_name insert}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+        (find_index (equal x) args, NONE) :: aux y
+    | Const (@{const_name Cons}, _) $ (Const (@{const_name atom}, _) $ (x as Var _)) $ y =>
+        (find_index (equal x) args, NONE) :: aux y
+    | Const (@{const_name bot}, _) => []
+    | Const (@{const_name Nil}, _) => []
+    | (f as Const _) $ (x as Var _) => [(find_index (equal x) args, SOME f)]
+    | _ => error ("Unsupported binding function: " ^ (Syntax.string_of_term lthy t))
+in
+  aux t
+end  
 *}
 
 ML {*
@@ -190,15 +195,14 @@
   fun aux eq = 
   let
     val (lhs, rhs) = eq
-      |> strip_qnt_body "all" 
       |> HOLogic.dest_Trueprop
       |> HOLogic.dest_eq
     val (bn_fun, [cnstr]) = strip_comb lhs
-    val (_, ty) = dest_Free bn_fun
+    val (_, ty) = dest_Const bn_fun
     val (ty_name, _) = dest_Type (domain_type ty)
     val dt_index = find_index (fn x => x = ty_name) dt_names
-    val (cnstr_head, cnstr_args) = strip_comb cnstr
-    val rhs_elements = strip_bn_fun rhs
+    val (cnstr_head, cnstr_args) = strip_comb cnstr    
+    val rhs_elements = strip_bn_fun lthy cnstr_args rhs
     val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
@@ -250,18 +254,18 @@
     (bn_fun_strs ~~ bn_fun_strs')
   
   val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
+  val raw_dt_names' =  map (Long_Name.qualify thy_name) raw_dt_names
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
-  val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_env binds 
-  val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+  val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
+  (*val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs)*)
 
-  val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
+  val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
   val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
 
-  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
-  fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
-  val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr;
+  val raw_bn_descr = 
+    prep_bn_descr lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs2)
 in
-  (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy1)
+  (raw_dt_full_names, raw_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr, lthy2)
 end
 *}
 
@@ -305,19 +309,11 @@
 ML {*
 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_bclauses, raw_bn_funs2, raw_bn_eqs2, raw_bn_funs, raw_bn_eqs, raw_bn_descr, raw_bn_descr2, lthy1) =
+  (* definition of the raw datatypes *)
+  val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_descr, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr)
-  val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2)
-  val _ = tracing ("raw_bclauses " ^ @{make_string} raw_bclauses)
-  val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs)
-  val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs)
-  val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2)
-  val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2))
-
   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
@@ -349,7 +345,7 @@
 
   val (fv, fvbn, fv_def, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) raw_bn_funs2) (map snd raw_bn_eqs2) descr sorts raw_bn_descr2 raw_bn_descr2 raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bn_funs raw_bn_descr raw_bclauses lthy3
     else raise TEST lthy3
   
 
@@ -362,9 +358,9 @@
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) descr;
-  val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
+  val bn_tys = map (domain_type o fastype_of) [] (*raw_bn_funs;*)
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
-  val bns = raw_bn_funs ~~ bn_nos;
+  val bns = [] (*raw_bn_funs*) ~~ bn_nos;
   val rel_dists = flat (map (distinct_rel lthy4 alpha_cases)
     (rel_distinct ~~ alpha_ts_nobn));
   val rel_dists_bn = flat (map (distinct_rel lthy4 alpha_cases)
@@ -376,7 +372,7 @@
   
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm (raw_bn_eqs @ raw_perm_defs) (map fst bns) lthy4
+  val (bv_eqvt, lthy5) = prove_eqvt all_tys induct_thm ((*raw_bn_eqs @*) raw_perm_defs) (map fst bns) lthy4
   val (fv_eqvt, lthy6) = prove_eqvt all_tys induct_thm (fv_def @ raw_perm_defs) (fv @ fvbn) lthy5
   val (alpha_eqvt, lthy6a) = Nominal_Eqvt.equivariance alpha_ts alpha_induct alpha_intros lthy6;
 
@@ -400,7 +396,7 @@
           Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
-  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
+  val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct [] (*raw_bn_eqs*) (map fst bns) lthy8;
   val (bns_rsp_pre, lthy9) = fold_map (
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
@@ -429,7 +425,7 @@
   val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (fv @ fvbn)) lthy12;
   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 (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
+  val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ [] (*raw_bn_funs*)) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
   val (qalpha_ts_bn, qalphabn_defs, lthy12c) = 
     quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
@@ -456,7 +452,7 @@
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
   val q_fv = map (lift_thm qtys lthy15) fv_def;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
+  val q_bn = map (lift_thm qtys lthy16) [] (*raw_bn_eqs;*)
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
@@ -575,7 +571,7 @@
   fun prep_binder env bn_str =
     case (Syntax.read_term lthy bn_str) of
       Free (x, _) => (NONE, index_lookup env x)
-    | Const (a, T) $ Free (x, _) => (SOME (Free (Long_Name.base_name a, T)), index_lookup env x)
+    | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x)
     | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.")
  
   fun prep_body env bn_str = index_lookup env bn_str