# HG changeset patch
# User wenzelm
# Date 1152651636 -7200
# Node ID bc3f9cb336458d12113c7ab8a7e016836286b575
# Parent  19871ee094b115d6220eb3e535c5a23fc3f59828
clean: no special treatment of empty name;
declare, invent: clean arguments;

diff -r 19871ee094b1 -r bc3f9cb33645 src/Pure/name.ML
--- a/src/Pure/name.ML	Tue Jul 11 23:00:35 2006 +0200
+++ b/src/Pure/name.ML	Tue Jul 11 23:00:36 2006 +0200
@@ -56,11 +56,10 @@
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
 
-fun clean_index ("", i) = ("u", i + 1)
-  | clean_index (x, i) =
-      (case try dest_internal x of
-        NONE => (x, i)
-      | SOME x' => clean_index (x', i + 1));
+fun clean_index (x, i) =
+  (case try dest_internal x of
+    NONE => (x, i)
+  | SOME x' => clean_index (x', i + 1));
 
 fun clean x = #1 (clean_index (x, 0));
 
@@ -73,8 +72,11 @@
 datatype context =
   Context of string option Symtab.table;    (*declared names with latest renaming*)
 
-fun declare x (Context tab) = Context (Symtab.default (x, NONE) tab);
-fun declare_renaming (x, x') (Context tab) = Context (Symtab.update (x, SOME x') tab);
+fun declare x (Context tab) =
+  Context (Symtab.default (clean x, NONE) tab);
+
+fun declare_renaming (x, x') (Context tab) =
+  Context (Symtab.update (clean x, SOME (clean x')) tab);
 
 fun declared (Context tab) = Symtab.lookup tab;
 
@@ -92,7 +94,7 @@
             if is_some (declared ctxt x) then invs x' n
             else x :: invs x' (n - 1)
           end;
-  in invs end;
+  in invs o clean end;
 
 val invent_list = invents o make_context;