# HG changeset patch
# User haftmann
# Date 1256285516 -7200
# Node ID fe29679cabc23a34bebb7e8ca6a25928d7720260
# Parent  c6693f51e4e4fbec1435d6cdab65895ea61cf036# Parent  180feec9acf6a341dce24c2639cbef335dacff6d
merged

diff -r c6693f51e4e4 -r fe29679cabc2 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Oct 23 06:53:50 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Oct 23 10:11:56 2009 +0200
@@ -209,6 +209,8 @@
 fun make_bool_args' xs =
   make_bool_args (K HOLogic.false_const) (K HOLogic.true_const) xs;
 
+fun arg_types_of k c = Library.drop (k, binder_types (fastype_of c));
+
 fun find_arg T x [] = sys_error "find_arg"
   | find_arg T x ((p as (_, (SOME _, _))) :: ps) =
       apsnd (cons p) (find_arg T x ps)
@@ -231,8 +233,7 @@
     val i = find_index (fn c' => c' = c) cs;
   in
     if xs = params andalso i >= 0 then
-      SOME (c, i, ys, chop (length ys)
-        (List.drop (binder_types (fastype_of c), k)))
+      SOME (c, i, ys, chop (length ys) (arg_types_of k c))
     else NONE
   end;
 
@@ -383,7 +384,7 @@
 
     fun prove_elim c =
       let
-        val Ts = List.drop (binder_types (fastype_of c), length params);
+        val Ts = arg_types_of (length params) c;
         val (anames, ctxt'') = Variable.variant_fixes (mk_names "a" (length Ts)) ctxt';
         val frees = map Free (anames ~~ Ts);
 
@@ -493,9 +494,8 @@
     val (pnames, ctxt') = ctxt |>
       Variable.add_fixes (map (fst o dest_Free) params) |> snd |>
       Variable.variant_fixes (mk_names "P" (length cs));
-    val preds = map Free (pnames ~~
-      map (fn c => List.drop (binder_types (fastype_of c), length params) --->
-        HOLogic.boolT) cs);
+    val preds = map2 (curry Free) pnames
+      (map (fn c => arg_types_of (length params) c ---> HOLogic.boolT) cs);
 
     (* transform an introduction rule into a premise for induction rule *)
 
@@ -591,15 +591,11 @@
 
 (** specification of (co)inductive predicates **)
 
-fun drop_first f [] = []
-  | drop_first f (x :: xs) = if f x then xs else x :: drop_first f xs;
-
 fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
   let
     val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
 
-    val argTs = fold (fn c => fn Ts => Ts @
-      (fold (fn T => drop_first (curry (op =) T)) Ts (List.drop (binder_types (fastype_of c), length params)))) cs [];
+    val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
     val k = log 2 1 (length cs);
     val predT = replicate k HOLogic.boolT ---> argTs ---> HOLogic.boolT;
     val p :: xs = map Free (Variable.variant_frees ctxt intr_ts
@@ -663,7 +659,7 @@
     val specs = if length cs < 2 then [] else
       map_index (fn (i, (name_mx, c)) =>
         let
-          val Ts = List.drop (binder_types (fastype_of c), length params);
+          val Ts = arg_types_of (length params) c;
           val xs = map Free (Variable.variant_frees ctxt intr_ts
             (mk_names "x" (length Ts) ~~ Ts))
         in
diff -r c6693f51e4e4 -r fe29679cabc2 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Oct 23 06:53:50 2009 +0200
+++ b/src/Pure/library.ML	Fri Oct 23 10:11:56 2009 +0200
@@ -173,6 +173,7 @@
 
   (*lists as multisets*)
   val remove1: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
+  val combine: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
   val submultiset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
 
   (*orders*)
@@ -858,8 +859,10 @@
 
 (** lists as multisets **)
 
-fun remove1 _ _ [] = raise Empty
-  | remove1 eq y (x::xs) = if eq (y, x) then xs else x :: remove1 eq y xs;
+fun remove1 eq x [] = []
+  | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys;
+
+fun combine eq xs ys = fold (remove1 eq) ys xs @ ys;
 
 fun submultiset _ ([], _)  = true
   | submultiset eq (x :: xs, ys) = member eq ys x andalso submultiset eq (xs, remove1 eq x ys);