diff -r bcf558c445a4 -r 90779aefbf1a Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Dec 08 13:16:25 2010 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 08 17:07:08 2010 +0000
@@ -15,6 +15,47 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+ML {*
+fun strip_prems_concl trm =
+  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
+
+fun strip_outer_params (Const("all", _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
+  | strip_outer_params B = ([], B)
+*}
+
+ML {*
+fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
+  let
+    val (cses, main_concls) = qexhausts
+      |> map prop_of
+      |> map strip_prems_concl
+      |> split_list
+
+    fun process_case cse bclauses =
+      let
+        val (params, (body, concl)) = cse
+          |> strip_outer_params
+          ||> Logic.dest_implies
+      in
+        Logic.mk_implies (body, concl) 
+      end  
+  
+    val cses' = map2 (map2 process_case) cses bclausess
+      |> map (map (Syntax.string_of_term lthy))
+      |> map commas
+      |> cat_lines
+
+    val _ = tracing ("cases\n " ^ cses')
+  in
+    ()
+  end
+*}
+
+ML {*
+val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
+val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
+val simp_attr = Attrib.internal (K Simplifier.simp_add)
+*}
 
 section{* Interface for nominal_datatype *}
 
@@ -165,6 +206,7 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  val _ = tracing ("bclauses\n" ^ cat_lines (map @{make_string} bclauses))
   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)
@@ -524,6 +566,8 @@
     then prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qfv_qbn_eqvts lthyC
     else []
 
+  val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts qtrms bclauses
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)