# HG changeset patch
# User wenzelm
# Date 1152790922 -7200
# Node ID 88fa4127382471c2a218280e6f2be6fa07b49ea3
# Parent  27255556b7623a8928b8fafd012748158fbc510a
Name.context already declares empty names;
tune ins_sorts -- sort assigments should never change later;

diff -r 27255556b762 -r 88fa41273824 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jul 13 13:42:00 2006 +0200
+++ b/src/Pure/variable.ML	Thu Jul 13 13:42:02 2006 +0200
@@ -77,7 +77,7 @@
   val name = "Pure/variable";
   type T = data;
   fun init thy =
-    make_data (false, Name.make_context ["", "'"], [], Vartab.empty,
+    make_data (false, Name.context, [], Vartab.empty,
       (Vartab.empty, Vartab.empty, [], Symtab.empty));
   fun print _ _ = ();
 );
@@ -148,8 +148,8 @@
     | _ => I);
 
 val ins_sorts = fold_atyps
-  (fn TFree (x, S) => Vartab.update ((x, ~1), S)
-    | TVar v => Vartab.update v
+  (fn TFree (x, S) => Vartab.default ((x, ~1), S)
+    | TVar v => Vartab.default v
     | _ => I);
 
 val ins_used = fold_atyps