# HG changeset patch
# User krauss
# Date 1219752944 -7200
# Node ID c8642f498aa3b35e22b7306d6c097b7c9e1cf8ee
# Parent  9c8d5e9101697e602649837941fc6f0e7c0fb750
function package: name primitive defs "f_sumC_def" instead of "f_sum_def" to avoid clashes

diff -r 9c8d5e910169 -r c8642f498aa3 src/HOL/SizeChange/Kleene_Algebras.thy
--- a/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Aug 26 12:20:52 2008 +0200
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Tue Aug 26 14:15:44 2008 +0200
@@ -452,7 +452,7 @@
 
 lemma mk_tcl_default: "\<not> mk_tcl_dom (a,x) \<Longrightarrow> mk_tcl a x = 0"
   unfolding mk_tcl_def
-  by (rule fundef_default_value[OF mk_tcl_sum_def graph_implies_dom])
+  by (rule fundef_default_value[OF mk_tcl_sumC_def graph_implies_dom])
 
 
 text {* We can replace the dom-Condition of the correctness theorem 
diff -r 9c8d5e910169 -r c8642f498aa3 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 12:20:52 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Tue Aug 26 14:15:44 2008 +0200
@@ -889,7 +889,7 @@
           PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
       val ((f, f_defthm), lthy) = 
-          PROFILE "def_fun" (define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default) lthy
+          PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
       val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
       val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees