1.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 12:20:52 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 14:15:44 2008 +0200
     1.3 @@ -889,7 +889,7 @@
     1.4            PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
     1.5  
     1.6        val ((f, f_defthm), lthy) = 
     1.7 -          PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
     1.8 +          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
     1.9  
    1.10        val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
    1.11        val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees