--- a/Nominal/Ex/Foo2.thy	Tue Dec 07 19:16:09 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Wed Dec 08 12:37:25 2010 +0000
@@ -30,6 +30,7 @@
 thm foo.perm_bn_simps
 thm foo.bn_finite
 
+
 thm foo.distinct
 thm foo.induct
 thm foo.inducts
@@ -45,12 +46,9 @@
 thm foo.supp
 thm foo.fresh
 
-text {*
-  tests by cu
-*}
 
 
-text {* *}
+
 
 
 (*
@@ -71,6 +69,25 @@
 sorry 
 *)
 
+thm foo.exhaust
+
+ML {*
+fun strip_prems_concl trm =
+  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+*}
+
+
+ML {*
+  @{thms foo.exhaust}
+  |> map prop_of
+  |> map strip_prems_concl
+  |> map fst
+  |> map (map (Syntax.string_of_term @{context}))
+  |> map cat_lines
+  |> cat_lines
+  |> writeln 
+*}
+
 lemma test6:
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 

--- a/Nominal/Nominal2.thy	Tue Dec 07 19:16:09 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 08 12:37:25 2010 +0000
@@ -200,7 +200,7 @@
 *}
 
 ML {*
-fun define_raw_dts dts bn_funs bn_eqs binds lthy =
+fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 let
   val thy = Local_Theory.exit_global lthy
   val thy_name = Context.theory_name thy
@@ -225,7 +225,7 @@
   
   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_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env bclauses 
 
   val (raw_dt_full_names, thy1) = 
     Datatype.add_datatype Datatype.default_config raw_dt_names raw_dts thy
@@ -258,6 +258,8 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  val _ = tracing ("raw_bclauses\n" ^ cat_lines (map @{make_string} raw_bclauses))
+
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
@@ -270,7 +272,7 @@
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) raw_full_ty_names  
  
   val raw_cns_info = all_dtyp_constrs_types descr sorts
-  val raw_constrs = flat (map (map (fn (c, _, _, _) => c)) raw_cns_info)
+  val raw_constrs = map (map (fn (c, _, _, _) => c)) raw_cns_info
 
   val raw_inject_thms = flat (map #inject dtinfos)
   val raw_distinct_thms = flat (map #distinct dtinfos)
@@ -286,7 +288,7 @@
   val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_simps, raw_perm_laws), lthy2a) =
     if get_STEPS lthy0 > 0 
-    then define_raw_perms raw_full_ty_names raw_tys tvs raw_constrs raw_induct_thm lthy0
+    then define_raw_perms raw_full_ty_names raw_tys tvs (flat raw_constrs) raw_induct_thm lthy0
     else raise TEST lthy0
  
   (* noting the raw permutations as eqvt theorems *)
@@ -419,7 +421,7 @@
 
   val raw_constrs_rsp = 
     if get_STEPS lthy > 18
-    then raw_constrs_rsp raw_constrs alpha_trms alpha_intros
+    then raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
       (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
     else raise TEST lthy6 
 
@@ -462,9 +464,8 @@
 
   (* defining of quotient term-constructors, binding functions, free vars functions *)
   val _ = warning "Defining the quotient constants"
-  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)) raw_constrs
+  val qconstrs_descrs =
+    map2 (map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx))) (get_cnstrs dts) raw_constrs
 
   val qbns_descr =
     map2 (fn (b, _, mx) => fn t => (Name.of_binding b, t, mx)) bn_funs raw_bns
@@ -487,12 +488,12 @@
   val qperm_bn_descr = 
     map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
      
-
-  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), lthy8)= 
+  val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
+    lthy8) = 
     if get_STEPS lthy > 24
     then 
       lthy7
-      |> define_qconsts qtys qconstrs_descr 
+      |> fold_map (define_qconsts qtys) qconstrs_descrs 
       ||>> define_qconsts qtys qbns_descr 
       ||>> define_qconsts qtys qfvs_descr
       ||>> define_qconsts qtys qfv_bns_descr
@@ -511,7 +512,7 @@
     then define_qsizes qtys qty_full_names tvs qsize_descr lthy9
     else raise TEST lthy9
 
-  val qtrms = map #qconst qconstrs_info
+  val qtrms = map (map #qconst) qconstrs_infos
   val qbns = map #qconst qbns_info
   val qfvs = map #qconst qfvs_info
   val qfv_bns = map #qconst qfv_bns_info
@@ -554,7 +555,7 @@
   val _ = warning "Proving Supports Lemmas and fs-Instances"
   val qsupports_thms =
     if get_STEPS lthy > 29
-    then prove_supports lthyB qperm_simps qtrms
+    then prove_supports lthyB qperm_simps (flat qtrms)
     else raise TEST lthyB
 
   (* finite supp lemmas *)
@@ -573,7 +574,7 @@
   val _ = warning "Proving Equality between fv and supp"
   val qfv_supp_thms = 
     if get_STEPS lthy > 32
-    then prove_fv_supp qtys qtrms qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
+    then prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []