# HG changeset patch
# User wenzelm
# Date 1121435062 -7200
# Node ID cf7d61d56acf205d51f762647975fccdf171b3cc
# Parent  cde0b6864924e0ad6cf27498937e3c4c582037ab
tuned fold on terms and lists;

diff -r cde0b6864924 -r cf7d61d56acf src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Fri Jul 15 15:44:21 2005 +0200
+++ b/src/ZF/ind_syntax.ML	Fri Jul 15 15:44:22 2005 +0200
@@ -124,18 +124,13 @@
     let val rec_hds = map head_of rec_tms
         val dummy = assert_all is_Const rec_hds
           (fn t => "Datatype set not previously declared as constant: " ^
-                   Sign.string_of_term (sign_of IFOL.thy) t);
+                   Sign.string_of_term IFOL.thy t);
         val rec_names = (*nat doesn't have to be added*)
 	    "Nat.nat" :: map (#1 o dest_Const) rec_hds
 	val u = if co then quniv else univ
-	fun is_OK (Const(a,T)) = not (a mem_string rec_names)
-	  | is_OK _            = false
-	val add_term_consts_2 =
-	    foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs);
-	fun fourth (_, name, args, prems) = prems
-	fun add_consts_in_cts cts = 
-	    Library.foldl (Library.foldl add_term_consts_2) ([], map fourth (List.concat cts));
-	val cs = List.filter is_OK (add_consts_in_cts con_ty_lists)
+	val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
+          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
+            | _ => I)) con_ty_lists [];
     in  u $ union_params (hd rec_tms, cs)  end;