src/Pure/name.ML
changeset 20099 bc3f9cb33645
parent 20089 d757ebadb0a2
child 20104 f8e7c71926e4
     1.1 --- a/src/Pure/name.ML	Tue Jul 11 23:00:35 2006 +0200
     1.2 +++ b/src/Pure/name.ML	Tue Jul 11 23:00:36 2006 +0200
     1.3 @@ -56,11 +56,10 @@
     1.4  val skolem = suffix "__";
     1.5  val dest_skolem = unsuffix "__";
     1.6  
     1.7 -fun clean_index ("", i) = ("u", i + 1)
     1.8 -  | clean_index (x, i) =
     1.9 -      (case try dest_internal x of
    1.10 -        NONE => (x, i)
    1.11 -      | SOME x' => clean_index (x', i + 1));
    1.12 +fun clean_index (x, i) =
    1.13 +  (case try dest_internal x of
    1.14 +    NONE => (x, i)
    1.15 +  | SOME x' => clean_index (x', i + 1));
    1.16  
    1.17  fun clean x = #1 (clean_index (x, 0));
    1.18  
    1.19 @@ -73,8 +72,11 @@
    1.20  datatype context =
    1.21    Context of string option Symtab.table;    (*declared names with latest renaming*)
    1.22  
    1.23 -fun declare x (Context tab) = Context (Symtab.default (x, NONE) tab);
    1.24 -fun declare_renaming (x, x') (Context tab) = Context (Symtab.update (x, SOME x') tab);
    1.25 +fun declare x (Context tab) =
    1.26 +  Context (Symtab.default (clean x, NONE) tab);
    1.27 +
    1.28 +fun declare_renaming (x, x') (Context tab) =
    1.29 +  Context (Symtab.update (clean x, SOME (clean x')) tab);
    1.30  
    1.31  fun declared (Context tab) = Symtab.lookup tab;
    1.32  
    1.33 @@ -92,7 +94,7 @@
    1.34              if is_some (declared ctxt x) then invs x' n
    1.35              else x :: invs x' (n - 1)
    1.36            end;
    1.37 -  in invs end;
    1.38 +  in invs o clean end;
    1.39  
    1.40  val invent_list = invents o make_context;
    1.41