Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Name.context already declares empty names;
authorwenzelm
Thu, 13 Jul 2006 13:42:02 +0200
changeset 20123 88fa41273824
parent 20122 27255556b762
child 20124 caf3a129b90d
Name.context already declares empty names; tune ins_sorts -- sort assigments should never change later;
src/Pure/variable.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle