diff -r c5a8b612e571 -r 0040bafffdef src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Jul 01 16:54:44 2010 +0200
@@ -39,17 +39,17 @@
 fun constant_0 T = Abs ("x", T, HOLogic.zero)
 fun constant_1 T = Abs ("x", T, HOLogic.Suc_zero)
 
-fun mk_funorder_funs (Type (@{type_name "+"}, [fT, sT])) =
+fun mk_funorder_funs (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
   map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT m (constant_0 sT)) (mk_funorder_funs fT)
   @ map (fn m => SumTree.mk_sumcase fT sT HOLogic.natT (constant_0 fT) m) (mk_funorder_funs sT)
   | mk_funorder_funs T = [ constant_1 T ]
 
-fun mk_ext_base_funs ctxt (Type (@{type_name "+"}, [fT, sT])) =
+fun mk_ext_base_funs ctxt (Type (@{type_name Sum_Type.sum}, [fT, sT])) =
     map_product (SumTree.mk_sumcase fT sT HOLogic.natT)
       (mk_ext_base_funs ctxt fT) (mk_ext_base_funs ctxt sT)
   | mk_ext_base_funs ctxt T = find_measures ctxt T
 
-fun mk_all_measure_funs ctxt (T as Type (@{type_name "+"}, _)) =
+fun mk_all_measure_funs ctxt (T as Type (@{type_name Sum_Type.sum}, _)) =
     mk_ext_base_funs ctxt T @ mk_funorder_funs T
   | mk_all_measure_funs ctxt T = find_measures ctxt T