# HG changeset patch
# User haftmann
# Date 1121244501 -7200
# Node ID 54b5df61065180236dc61c6d88de4f1cc4639c78
# Parent  2eddcce4fd1614af1aac61e831f32fbf1f9b5cdd
(corrected wrong commit)

diff -r 2eddcce4fd16 -r 54b5df610651 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jul 13 10:44:51 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jul 13 10:48:21 2005 +0200
@@ -178,8 +178,8 @@
 fun unify_consts thy cs intr_ts =
   (let
     val tsig = Sign.tsig_of thy;
-    fun add_term_consts_2 (x, y) =
-      fold_aterms (fn (Const c) => curry (op ins) c | _ => I) y x;
+    val add_term_consts_2 =
+      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
     fun varify (t, (i, ts)) =
       let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
       in (maxidx_of_term t', t'::ts) end;