--- a/Nominal/Ex/Test.thy	Sun May 16 12:41:27 2010 +0100
+++ b/Nominal/Ex/Test.thy	Mon May 17 12:00:54 2010 +0100
@@ -5,6 +5,8 @@
 (* This file contains only the examples that are not supposed to work yet. *)
 
 
+declare [[STEPS = 2]]
+
 atom_decl name
 
 (* example 4 from Terms.thy *)
@@ -12,12 +14,11 @@
    defined fv and defined alpha... *)
 (* lists-datastructure does not work yet *)
 
-(*
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm list"
 | Lm x::"name" t::"trm"  bind x in t
-*)
+
 
 (*
 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

--- a/Nominal/NewParser.thy	Sun May 16 12:41:27 2010 +0100
+++ b/Nominal/NewParser.thy	Mon May 17 12:00:54 2010 +0100
@@ -67,8 +67,9 @@
 
 
 ML {* 
+(* exports back the results *)
 fun add_primrec_wrapper funs eqs lthy = 
-  if null funs then (([], []), lthy)
+  if null funs then ([], [], lthy)
   else 
    let 
      val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
@@ -76,7 +77,7 @@
      val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy
      val phi = ProofContext.export_morphism lthy' lthy
    in 
-     ((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy')
+     (map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs'', lthy')
    end
 *}
 
@@ -162,9 +163,9 @@
 end
 *}
 
-(* strip_bn_fun takes a bn function defined by the user as a union or
-   append of elements and returns those elements together with bn functions
-   applied *)
+(* strip_bn_fun takes a rhs of a bn function: this can only contain unions or
+   appends of elements; in case of recursive calls it retruns also the applied
+   bn function *)
 ML {*
 fun strip_bn_fun t =
   case t of
@@ -226,7 +227,6 @@
 end
 *}
 
-ML {* add_primrec_wrapper *}
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
@@ -252,14 +252,12 @@
     (bn_fun_strs ~~ bn_fun_strs')
   
   val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
-
   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_full_env binds 
   val raw_bns = prep_bn 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_bn_funs, raw_bn_eqs), lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+  val (raw_bn_funs, raw_bn_eqs, 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);
@@ -370,22 +368,19 @@
 
 setup STEPS_setup
 
-
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
-  (* definition of the raw datatype and raw bn-functions *)
+  (* definition of the raw datatypes and raw bn-functions *)
   val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
     if get_STEPS lthy > 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 dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
+  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
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames
   
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
@@ -395,13 +390,14 @@
   val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
-  val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    if get_STEPS lthy > 2 
+  val ((perms, raw_perm_defs, raw_perm_simps), lthy2) =
+    if get_STEPS lthy1 > 2 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
 
   val (_, lthy2a) = Local_Theory.note ((Binding.empty,
-    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
+    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_defs) lthy2;
+
   val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
 
@@ -410,7 +406,7 @@
   val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
   val ((fv, fvbn), fv_def, lthy3a) = 
-    if get_STEPS lthy > 3 
+    if get_STEPS lthy2 > 3 
     then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
     else raise TEST lthy3
   
@@ -439,8 +435,8 @@
 
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
-  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
+  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;
 
   (* proving alpha equivalence *)
@@ -454,7 +450,7 @@
   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
-  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6a;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_tys alpha_ts_nobn alpha_equivp lthy6a;
   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)) =>
@@ -515,7 +511,7 @@
     [Rule_Cases.name constr_names q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length fv)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-  val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
+  val q_perm = map (lift_thm qtys lthy14) raw_perm_defs;
   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;

--- a/Nominal/Perm.thy	Sun May 16 12:41:27 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 17 12:00:54 2010 +0100
@@ -146,17 +146,20 @@
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
   
-  fun tac _ (_, simps, _) =
+  fun tac _ (_, _, simps) =
     Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
   
-  fun morphism phi (dfs, simps, fvs) =
-    (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
+  fun morphism phi (fvs, dfs, simps) =
+    (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps);
+
+  val eqvt_attrib = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 in
   lthy'
+  (*|> snd o (Local_Theory.note ((Binding.empty, [eqvt_attrib]), perm_eq_thms))*)
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
   |> Class_Target.prove_instantiation_exit_result morphism tac 
-       (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
+       (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms')
 end
 *}