diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/Tools/function_package/sum_tools.ML
--- a/src/HOL/Tools/function_package/sum_tools.ML	Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/Tools/function_package/sum_tools.ML	Wed Sep 13 12:05:50 2006 +0200
@@ -17,6 +17,7 @@
   val projr_inr: thm
 
   val mk_tree : typ list -> typ * sum_tree * sum_path list
+  val mk_tree_distinct : typ list -> typ * sum_tree * sum_path list
 
   val mk_proj: sum_tree -> sum_path -> term -> term
   val mk_inj: sum_tree -> sum_path -> term -> term
@@ -37,12 +38,9 @@
 val projl_inl = thm "FunDef.lproj_inl"
 val projr_inr = thm "FunDef.rproj_inr"
 
-
-
 fun mk_sumT LT RT = Type ("+", [LT, RT])
 fun mk_sumcase TL TR T l r = Const (sumcaseN, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
 
-
 datatype sum_tree 
   = Leaf of typ
   | Branch of (typ * (typ * sum_tree) * (typ * sum_tree))
@@ -72,6 +70,23 @@
     end
 
 
+fun mk_tree_distinct Ts =
+    let
+      fun insert_once T Ts =
+          let
+            val i = find_index_eq T Ts
+          in
+            if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts)
+          end
+
+      val (idxs, dist_Ts) = fold_map insert_once Ts []
+
+      val (ST, tree, pths) = mk_tree dist_Ts
+    in
+      (ST, tree, map (nth pths) idxs)
+    end
+
+
 fun mk_inj (Leaf _) [] t = t
   | mk_inj (Branch (ST, (LT, tr), _)) (true::pth) t = 
     Const (inlN, LT --> ST) $ mk_inj tr pth t