--- a/Nominal/Nominal2.thy	Fri Dec 10 19:01:44 2010 +0000
+++ b/Nominal/Nominal2.thy	Sun Dec 12 00:10:40 2010 +0000
@@ -15,6 +15,8 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+text {* TEST *}
+
 ML {*
 fun strip_prems_concl trm =
   (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
@@ -23,10 +25,29 @@
   | strip_outer_params B = ([], B)
 *}
 
+
+ML {*
+fun binders bclauses = 
+  let
+    fun aux1 (NONE, i) = Bound i 
+      | aux1 (SOME bn, i) = bn $ Bound i         
+  in
+    bclauses
+    |> map (fn (BC (_, x, _)) => x)
+    |> flat
+    |> map aux1
+  end
+*}
+
 ML {*
 fun prove_strong_exhausts lthy qexhausts qtrms bclausess =
   let
-    val (cses, main_concls) = qexhausts
+    val ((_, qexhausts'), lthy') = Variable.import true qexhausts lthy 
+
+    val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy'
+    val c = Free (c, TFree (a, @{sort fs}))
+
+    val (cses, main_concls) = qexhausts'
       |> map prop_of
       |> map strip_prems_concl
       |> split_list
@@ -36,12 +57,15 @@
         val (params, (body, concl)) = cse
           |> strip_outer_params
           ||> Logic.dest_implies
+        
+        (*val bnds = HOLogic.mk_tuple (binders bclauses)*)
+        val prem = HOLogic.mk_Trueprop (HOLogic.mk_eq (c, c))
       in
-        Logic.mk_implies (body, concl) 
+        Logic.mk_implies (prem, Logic.mk_implies (body, concl)) 
       end  
   
     val cses' = map2 (map2 process_case) cses bclausess
-      |> map (map (Syntax.string_of_term lthy))
+      |> map (map (Syntax.string_of_term lthy''))
       |> map commas
       |> cat_lines