--- a/Nominal-General/nominal_library.ML	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal-General/nominal_library.ML	Fri Nov 12 01:20:53 2010 +0000
@@ -258,22 +258,37 @@
 
 fun prove_termination_tac size_simps ctxt =
   let
-    fun mk_size_measure (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
-        SumTree.mk_sumcase fT sT @{typ nat} (mk_size_measure fT) (mk_size_measure sT)
-      | mk_size_measure T = size_const T
+    val natT = @{typ nat}
+    fun prod_size_const fT sT = 
+      let
+        val fT_fun = fT --> natT
+        val sT_fun = sT --> natT
+        val prodT = Type (@{type_name prod}, [fT, sT])
+      in
+        Const (@{const_name prod_size}, [fT_fun, sT_fun, prodT] ---> natT)
+      end
+
+    fun mk_size_measure T =
+      case T of    
+        (Type (@{type_name Sum_Type.sum}, [fT, sT])) =>
+           SumTree.mk_sumcase fT sT natT (mk_size_measure fT) (mk_size_measure sT)
+      | (Type (@{type_name Product_Type.prod}, [fT, sT])) =>
+           prod_size_const fT sT $ (mk_size_measure fT) $ (mk_size_measure sT)
+      | _ => size_const T
 
     fun mk_measure_trm T = 
       HOLogic.dest_setT T
       |> fst o HOLogic.dest_prodT
       |> mk_size_measure 
-      |> curry (op $) (Const (@{const_name measure}, dummyT))
+      |> curry (op $) (Const (@{const_name "measure"}, dummyT))
       |> Syntax.check_term ctxt
-
+      
     val ss = HOL_ss addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
-      zero_less_Suc} @ size_simps addsimprocs Nat_Numeral_Simprocs.cancel_numerals
+      zero_less_Suc prod.size(1) mult_Suc_right} @ size_simps 
+    val ss' = ss addsimprocs Nat_Numeral_Simprocs.cancel_numerals
   in
     Function_Relation.relation_tac ctxt mk_measure_trm
-    THEN_ALL_NEW simp_tac ss
+    THEN_ALL_NEW simp_tac ss'
   end
 
 fun prove_termination size_simps ctxt =