--- a/Nominal-General/nominal_atoms.ML	Tue May 04 16:29:11 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Tue May 04 16:33:38 2010 +0200
@@ -58,7 +58,7 @@
       Specification.definition (NONE, ((permute_def_name, []), permute_eqn)) lthy;
     val ((_, (_, atom_ldef)), lthy) =
       Specification.definition (NONE, ((atom_def_name, []), atom_eqn)) lthy;
-    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);
+    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy);
     val permute_def = singleton (ProofContext.export lthy ctxt_thy) permute_ldef;
     val atom_def = singleton (ProofContext.export lthy ctxt_thy) atom_ldef;
     val class_thm = @{thm at_class} OF [type_definition, atom_def, permute_def];

--- a/Nominal/NewFv.thy	Tue May 04 16:29:11 2010 +0200
+++ b/Nominal/NewFv.thy	Tue May 04 16:33:38 2010 +0200
@@ -4,6 +4,8 @@
 begin
 
 ML {*
+(* binding modes *)
+
 datatype bmodes =
    BEmy of int
 |  BLst of ((term option * int) list) * (int list)
@@ -243,18 +245,19 @@
 *}
 
 ML {*
-fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy =
+fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr as dt_descr, sorts, ...} = dt_info;
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
+  val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
 
+  (* free variables for the bn-functions *)
   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
+  
   val fv_bns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
 

--- a/Nominal/NewParser.thy	Tue May 04 16:29:11 2010 +0200
+++ b/Nominal/NewParser.thy	Tue May 04 16:33:38 2010 +0200
@@ -350,31 +350,45 @@
  29) prove supp = fv
 *}
 
+ML {*
+(* for testing porposes - to exit the procedure early *)
+exception TEST of Proof.context
+
+val STEPS = 10
+*}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatype and raw bn-functions *)
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
-    raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    else raise TEST lthy
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
   val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
-  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
-  val inject = flat (map #inject dtinfos);
-  val distincts = flat (map #distinct dtinfos);
-  val rel_dtinfos = List.take (dtinfos, (length dts));
-  val rel_distinct = map #distinct rel_dtinfos;
-  val induct = #induct dtinfo;
-  val exhausts = map #exhaust dtinfos;
+  
+  (* what is the difference between raw_dt_names and all_full_tnames ? *)
+  (* what is the purpose of dtinfo and dtinfos ? *)
+  val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
+  val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
+
+  val inject_thms = flat (map #inject dtinfos);
+  val distinct_thms = flat (map #distinct dtinfos);
+  val rel_dtinfos = List.take (dtinfos, (length dts)); 
+  val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
+  val induct_thm = #induct dtinfo;
+  val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+    if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
+    else raise TEST lthy1
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
@@ -388,11 +402,18 @@
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   (* definition of raw fv_functions *)
-  val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
+  val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
+  val ((fv, fvbn), fv_def, lthy3a) = 
+    if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+    else raise TEST lthy3
   
+
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
-    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+    if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+    else raise TEST lthy3a
+  
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
@@ -405,27 +426,27 @@
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   
   (* definition of raw_alpha_eq_iff  lemmas *)
-  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
+  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);
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
-  (* provind alpha equivalence *)
+  (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff_simp lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
   val alpha_equivp =
     if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
     else build_equivps alpha_ts reflps alpha_induct
-      inject alpha_eq_iff_simp distincts alpha_cases alpha_eqvt lthy6;
+      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
@@ -455,7 +476,7 @@
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
     else
-      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     alpha_bn_rsp_tac) alpha_ts_bn lthy11
   fun const_rsp_tac _ =
@@ -480,7 +501,7 @@
   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 q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
+  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);
   fun note_simp_suffix s th ctxt =
@@ -529,7 +550,7 @@
   val lthy23 = note_suffix "supp" q_supp lthy22;
 in
   (0, lthy23)
-end
+end handle TEST ctxt => (0, ctxt)
 *}
 
 section {* Preparing and parsing of the specification *}
@@ -698,7 +719,7 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
-
+(*
 atom_decl name
 
 nominal_datatype lam =
@@ -715,6 +736,10 @@
   "bn (P1 x) = {atom x}"
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
+find_theorems Var_raw
+
+
+
 thm lam_pt.bn
 thm lam_pt.fv[simplified lam_pt.supp(1-2)]
 thm lam_pt.eq_iff

--- a/Nominal/Perm.thy	Tue May 04 16:29:11 2010 +0200
+++ b/Nominal/Perm.thy	Tue May 04 16:33:38 2010 +0200
@@ -116,9 +116,8 @@
    user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) user_dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
-  val {descr as dt_descr, induct, sorts, ...} = dt_info;
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
@@ -138,8 +137,8 @@
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = prove_permute_zero lthy' induct perm_eq_thms perm_funs
-  val perm_plus_thms = prove_permute_plus lthy' induct perm_eq_thms perm_funs
+  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
+  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
   val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
   val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
   val perms_name = space_implode "_" perm_fn_names

--- a/Nominal/Tacs.thy	Tue May 04 16:29:11 2010 +0200
+++ b/Nominal/Tacs.thy	Tue May 04 16:33:38 2010 +0200
@@ -158,9 +158,9 @@
 *}
 
 ML {*
-fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+fun dtyp_no_of_typ _ (TFree (_, _)) = error "dtyp_no_of_typ: Illegal free"
   | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
-  | dtyp_no_of_typ dts (Type (tname, Ts)) =
+  | dtyp_no_of_typ dts (Type (tname, _)) =
       case try (find_index (curry op = tname o fst)) dts of
         NONE => error "dtyp_no_of_typ: Illegal recursion"
       | SOME i => i