1.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Aug 26 12:20:52 2008 +0200
     1.2 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Aug 26 14:15:44 2008 +0200
     1.3 @@ -452,7 +452,7 @@
     1.4  
     1.5  lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
     1.6    unfolding mk_tcl_def
     1.7 -  by (rule fundef_default_value[OF mk_tcl_sum_def graph_implies_dom])
     1.8 +  by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
     1.9  
    1.10  
    1.11  text {* We can replace the dom-Condition of the correctness theorem 

     2.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 12:20:52 2008 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 14:15:44 2008 +0200
     2.3 @@ -889,7 +889,7 @@
     2.4            PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
     2.5  
     2.6        val ((f, f_defthm), lthy) = 
     2.7 -          PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
     2.8 +          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
     2.9  
    2.10        val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
    2.11        val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees