--- a/Nominal/nominal_dt_quot.ML	Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Tue Dec 28 00:20:50 2010 +0000
@@ -48,6 +48,8 @@
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
 struct
 
+fun lookup xs x = the (AList.lookup (op=) xs x)
+
 
 (* defines the quotient types *)
 fun define_qtypes qtys_descr alpha_tys alpha_trms alpha_equivp_thms lthy =
@@ -379,8 +381,8 @@
   end
 
 
-(** proves strong exhauts theorems **)
 
+(*** proves strong exhauts theorems ***)
 
 (* fixme: move into nominal_library *)
 fun abs_const bmode ty =
@@ -629,7 +631,7 @@
       |> HOLogic.mk_Trueprop 
       |> mk_all (c_name, c_ty)
 
-fun prep_prem lthy c (c_name, c_ty) bclauses (params, prems, concl) =
+fun prep_prem lthy c c_name c_ty bclauses (params, prems, concl) =
   let
     val tys = map snd params
     val binders = get_all_binders bclauses
@@ -686,15 +688,33 @@
 
     val prems' = prems
       |> map strip_full_horn
-      |> map2 (prep_prem lthy'' c (c_name, c_ty)) (flat bclausesss)
-      |> map (Syntax.check_term lthy'') 
+      |> map2 (prep_prem lthy'' c c_name c_ty) (flat bclausesss)
 
-    val _ = tracing ("induct:\n" ^ Syntax.string_of_term lthy'' (prop_of induct'))
-    val _ = tracing ("concls:\n" ^ commas (map (Syntax.string_of_term lthy'') concls))  
-    val _ = tracing ("prems':\n" ^ cat_lines (map (Syntax.string_of_term lthy'') prems'))
-
+    fun pat_tac ctxt thm =
+      Subgoal.FOCUS (fn {params, context, ...} => 
+        let
+          val thy = ProofContext.theory_of context
+          val ty_parms = map (fn (_, ct) => (fastype_of (term_of ct), ct)) params
+          val vs = Term.add_vars (prop_of thm) []
+          val vs_tys = map (Type.legacy_freeze_type o snd) vs
+          val vs_ctrms = map (cterm_of thy o Var) vs
+          val assigns = map (lookup ty_parms) vs_tys          
+          
+          val thm' = cterm_instantiate (vs_ctrms ~~ assigns) thm
+        in
+          rtac thm' 1
+        end) ctxt
+      THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss
+ 
     val thm = Goal.prove_multi lthy'' [] prems' concls
-      (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy''))
+      (fn {prems, context} => 
+        print_tac "start"
+        THEN Induction_Schema.induction_schema_tac context prems  
+        THEN print_tac "after induct schema"
+        THEN RANGE (map (pat_tac context) exhausts) 1
+        THEN print_tac "after pat"
+        THEN Skip_Proof.cheat_tac (ProofContext.theory_of context)
+      )
   in
     @{thm TrueI}
   end