function package: using the names of the equations as case names turned out to be impractical => disabled

--- a/src/HOL/NumberTheory/Fib.thy	Fri Nov 09 13:41:27 2007 +0100
+++ b/src/HOL/NumberTheory/Fib.thy	Fri Nov 09 18:59:56 2007 +0100
@@ -43,7 +43,7 @@
 next
   case 2 show ?case  by (simp add: fib_2)
 next
-  case fib_2 thus ?case by (simp add: fib.simps add_mult_distrib2)
+  case 3 thus ?case by (simp add: fib_2 add_mult_distrib2)
 qed
 
 lemma fib_Suc_neq_0: "fib (Suc n) \<noteq> 0"
@@ -72,9 +72,9 @@
 next
   case 2 thus ?case by (simp add: fib_2 mod_Suc)
 next 
-  case (fib_2 x) 
+  case (3 x) 
   have "Suc 0 \<noteq> x mod 2 \<longrightarrow> x mod 2 = 0" by presburger
-  with "fib_2.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
+  with "3.hyps" show ?case by (simp add: fib.simps add_mult_distrib add_mult_distrib2)
 qed
 
 text{*We now obtain a version for the natural numbers via the coercion 

--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Nov 09 13:41:27 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Nov 09 18:59:56 2007 +0100
@@ -282,7 +282,8 @@
       fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs)
                         |> map (map snd)
 
-      val cnames = map_index (fn (i, (n,_)) => mk_case_names i n 1) nas |> flat
+      (* using theorem names for case name currently disabled *)
+      val cnames = map_index (fn (i, (n,_)) => mk_case_names i "" 1) nas |> flat
     in
       (ts, curry op ~~ nas o Library.unflat tss, sort, cnames)
     end

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Nov 09 13:41:27 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Fri Nov 09 18:59:56 2007 +0100
@@ -280,7 +280,8 @@
 
           val nas' = nas @ replicate (length spliteqs - length nas) ("",[])
 
-          val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i n (length es)) 
+          (* using theorem names for case name currently disabled *)
+          val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es)) 
                                      (nas' ~~ spliteqs)
                            |> flat
         in