# HG changeset patch
# User haftmann
# Date 1255357004 -7200
# Node ID 84a5c684a22e092afa3fab2d4e957574e3134011
# Parent  dc48da9922bddd19ac3ea043ef840b5ed5b5ac00
added add_tyconames; tuned

diff -r dc48da9922bd -r 84a5c684a22e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 12 15:48:12 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 12 16:16:44 2009 +0200
@@ -51,6 +51,7 @@
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
   val add_constnames: iterm -> string list -> string list
+  val add_tyconames: iterm -> string list -> string list
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
 
   type naming
@@ -162,12 +163,22 @@
   of (IConst c, ts) => SOME (c, ts)
    | _ => NONE;
 
-fun add_constnames (IConst (c, _)) = insert (op =) c
-  | add_constnames (IVar _) = I
-  | add_constnames (t1 `$ t2) = add_constnames t1 #> add_constnames t2
-  | add_constnames (_ `|=> t) = add_constnames t
-  | add_constnames (ICase (((t, _), ds), _)) = add_constnames t
-      #> fold (fn (pat, body) => add_constnames pat #> add_constnames body) ds;
+fun fold_constexprs f =
+  let
+    fun fold' (IConst c) = f c
+      | fold' (IVar _) = I
+      | fold' (t1 `$ t2) = fold' t1 #> fold' t2
+      | fold' (_ `|=> t) = fold' t
+      | fold' (ICase (((t, _), ds), _)) = fold' t
+          #> fold (fn (pat, body) => fold' pat #> fold' body) ds
+  in fold' end;
+
+val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c);
+
+fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
+  | add_tycos (ITyVar _) = I;
+
+val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
 
 fun fold_varnames f =
   let