# HG changeset patch
# User wenzelm
# Date 1152613463 -7200
# Node ID 16e5b2723335b6fbf9215ff81b4057c110f1847f
# Parent  edc96f85e069b1efe5f6ce09cd93a88fbd5fa81f
Name.internal;
Name.invent_list;

diff -r edc96f85e069 -r 16e5b2723335 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Jul 11 12:22:58 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Jul 11 12:24:23 2006 +0200
@@ -1839,8 +1839,8 @@
 end;
 
 val _ = Context.add_setup
- (add_locale_i true "var" empty [Fixes [(Term.internal "x", NONE, NoSyn)]] #> snd #>
-  add_locale_i true "struct" empty [Fixes [(Term.internal "S", NONE, Structure)]] #> snd);
+ (add_locale_i true "var" empty [Fixes [(Name.internal "x", NONE, NoSyn)]] #> snd #>
+  add_locale_i true "struct" empty [Fixes [(Name.internal "S", NONE, Structure)]] #> snd);
 
 
 
@@ -2092,7 +2092,7 @@
            commas_quote (map Syntax.string_of_vname vars'));
     (* replace new types (which are TFrees) by ones with new names *)
     val new_Tnames = foldr Term.add_term_tfree_names [] vs;
-    val new_Tnames' = Term.invent_names used "'a" (length new_Tnames);
+    val new_Tnames' = Name.invent_list used "'a" (length new_Tnames);
     val renameT =
           if is_local then I
           else Logic.legacy_unvarifyT o Term.map_type_tfree (fn (a, s) =>