diff -r 29c1754b250f -r 645236e80885 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Mon Sep 25 17:04:46 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Sep 25 17:04:47 2006 +0200
@@ -54,12 +54,11 @@
     ((string * (inst list list * itype)) * iterm list) option;
   val add_constnames: iterm -> string list -> string list;
   val add_varnames: iterm -> string list -> string list;
+  val add_unbound_varnames: iterm -> string list -> string list;
   val is_pat: (string -> bool) -> iterm -> bool;
   val vars_distinct: iterm list -> bool;
   val map_pure: (iterm -> 'a) -> iterm -> 'a;
   val eta_expand: (string * (inst list list * itype)) * iterm list -> int -> iterm;
-  val resolve_tycos: (string -> string) -> itype * iterm list -> itype * iterm list;
-  val resolve_consts: (string -> string) -> iterm -> iterm;
 
   type typscheme = (vname * sort) list * itype;
   datatype def =
@@ -88,7 +87,6 @@
 (*   val flat_funs_datatypes: module -> (string * def) list;  *)
   val add_eval_def: string (*shallow name space*) * iterm -> module -> string * module;
   val delete_garbage: string list (*hidden definitions*) -> module -> module;
-  val has_nsp: string -> string -> bool;
   val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
     -> string -> transact -> transact;
   val succeed: 'a -> transact -> 'a transact_fin;
@@ -311,9 +309,6 @@
   | map_pure f (ICase (_, t0)) =
       f t0;
 
-fun resolve_tycos _ = error "";
-fun resolve_consts _ = error "";
-
 fun add_constnames (IConst (c, _)) =
       insert (op =) c
   | add_constnames (IVar _) =
@@ -344,6 +339,21 @@
   | add_varnames (ICase (((td, _), bs), _)) =
       add_varnames td #> fold (fn (p, t) => add_varnames p #> add_varnames t) bs;
 
+fun add_unbound_varnames (IConst _) =
+      I
+  | add_unbound_varnames (IVar v) =
+      insert (op =) v
+  | add_unbound_varnames (t1 `$ t2) =
+      add_unbound_varnames t1 #> add_unbound_varnames t2
+  | add_unbound_varnames ((v, _) `|-> t) =
+      I
+  | add_unbound_varnames (INum (_, t)) =
+      add_unbound_varnames t
+  | add_unbound_varnames (IChar (_, t)) =
+      add_unbound_varnames t
+  | add_unbound_varnames (ICase (((td, _), bs), _)) =
+      add_unbound_varnames td #> fold (fn (p, t) => add_unbound_varnames p #> add_unbound_varnames t) bs;
+
 fun vars_distinct ts =
   let
     fun distinct _ NONE =
@@ -513,14 +523,6 @@
   in (modl, NameSpace.pack [shallow, name_base]) end
   handle Empty => error ("Not a qualified name: " ^ quote name);
 
-fun has_nsp name shallow =
-  NameSpace.is_qualified name
-  andalso let
-    val name' = NameSpace.unpack name
-    val (name'', _) = split_last name'
-    val (_, shallow') = split_last name''
-  in shallow' = shallow end;
-
 fun dest_modl (Module m) = m;
 fun dest_def (Def d) = d;