--- 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