diff -r 7bc38b93a1fc -r 9ae285ce814e Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_library.ML	Fri May 16 08:38:23 2014 +0100
@@ -298,8 +298,7 @@
 (* decompses a formula into params, premises and a conclusion *)
 fun strip_full_horn trm =
   let
-    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = 
-      strip_outer_params t |>> cons (a, T)
+    fun strip_outer_params (Const (@{const_name Pure.all}, _) $ Abs (a, T, t)) = strip_outer_params t |>> cons (a, T)
     | strip_outer_params B = ([], B)
 
     val (params, body) = strip_outer_params trm
@@ -365,13 +364,13 @@
 
 val natT = @{typ nat}
     
-fun prod_size_const T1 T2 = 
+fun size_prod_const T1 T2 = 
   let
     val T1_fun = T1 --> natT
     val T2_fun = T2 --> natT
     val prodT = HOLogic.mk_prodT (T1, T2)
   in
-    Const (@{const_name prod_size}, [T1_fun, T2_fun, prodT] ---> natT)
+    Const (@{const_name size_prod}, [T1_fun, T2_fun, prodT] ---> natT)
   end
 
 fun snd_const T1 T2 =
@@ -409,7 +408,7 @@
       (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
          Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
     | (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
-         prod_size_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
+         size_prod_const T1 T2 $ (mk_size_measure T1) $ (mk_size_measure T2)
     | _ => HOLogic.size_const T
 
   val measure_trm = mk_measure_trm (mk_size_measure) ctxt