--- a/Nominal/nominal_dt_quot.ML	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/nominal_dt_quot.ML	Tue Dec 28 19:51:25 2010 +0000
@@ -42,7 +42,8 @@
   val prove_strong_exhausts: Proof.context -> thm list -> bclause list list list -> thm list -> 
     thm list -> thm list -> thm list -> thm list -> thm list
 
-  val prove_strong_induct: Proof.context -> thm -> thm list -> bclause list list list -> thm
+  val prove_strong_induct: Proof.context -> thm -> thm list -> thm list -> bclause list list list -> 
+    thm list
 end
 
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
@@ -668,7 +669,7 @@
     mk_full_horn (params @ [(c_name, c_ty)]) prems'' concl'
   end
 
-fun prove_strong_induct lthy induct exhausts bclausesss =
+fun prove_strong_induct lthy induct exhausts size_thms bclausesss =
   let
     val ((insts, [induct']), lthy') = Variable.import true [induct] lthy
 
@@ -706,17 +707,16 @@
         end) ctxt
       THEN_ALL_NEW asm_full_simp_tac HOL_basic_ss
  
-    val thm = Goal.prove_multi lthy'' [] prems' concls
+    val size_simp_tac = 
+      simp_tac (size_simpset addsimps (@{thms comp_def snd_conv} @ size_thms))
+  in
+    Goal.prove_multi lthy'' [] prems' concls
       (fn {prems, context} => 
-        print_tac "start"
-        THEN Induction_Schema.induction_schema_tac context prems  
-        THEN print_tac "after induct schema"
+        Induction_Schema.induction_schema_tac context prems  
         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}
+        THEN prove_termination_ind context 1
+        THEN ALLGOALS size_simp_tac)
+    |> ProofContext.export lthy'' lthy
   end