diff -r 040519ec99e9 -r b52e8651591f Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/nominal_library.ML	Thu Mar 13 09:21:31 2014 +0000
@@ -52,7 +52,7 @@
   val supp_rel_ty: typ -> typ
   val supp_rel_const: typ -> term
   val mk_supp_rel_ty: typ -> term -> term -> term
-  val mk_supp_rel: term -> term -> term		       
+  val mk_supp_rel: term -> term -> term
 
   val supports_const: typ -> term
   val mk_supports_ty: typ -> term -> term -> term
@@ -359,7 +359,7 @@
 val size_ss =
   simpset_of (put_simpset HOL_ss @{context}
    addsimprocs [@{simproc natless_cancel_numerals}]
-   addsimps @{thms in_measure wf_measure sum.cases add_Suc_right add.right_neutral 
+   addsimps @{thms in_measure wf_measure sum.case add_Suc_right add.right_neutral 
      zero_less_Suc prod.size(1) mult_Suc_right})
 
 val natT = @{typ nat}
@@ -374,7 +374,7 @@
   end
 
 fun snd_const T1 T2 =
-  Const ("Product_Type.snd", HOLogic.mk_prodT (T1, T2) --> T2) 
+  Const (@{const_name Product_Type.snd}, HOLogic.mk_prodT (T1, T2) --> T2) 
 
 
 fun mk_measure_trm f ctxt T = 
@@ -390,7 +390,7 @@
     fun mk_size_measure T =
       case T of    
         (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
-           SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
+           Sum_Tree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure T2)
       | (Type (@{type_name Product_Type.prod}, [T1, T2])) =>
            HOLogic.mk_comp (mk_size_measure T2, snd_const T1 T2)
       | _ => HOLogic.size_const T
@@ -406,7 +406,7 @@
   fun mk_size_measure T =
     case T of    
       (Type (@{type_name Sum_Type.sum}, [T1, T2])) =>
-         SumTree.mk_sumcase T1 T2 natT (mk_size_measure T1) (mk_size_measure 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)
     | _ => HOLogic.size_const T
@@ -512,4 +512,4 @@
 
 end (* structure *)
 
-open Nominal_Library;
\ No newline at end of file
+open Nominal_Library;