diff -r d28f549105fe -r 8f5767370f69 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Mon Feb 21 14:08:15 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Mon Feb 21 14:09:18 2000 +0100
@@ -44,9 +44,9 @@
 
 fun tagit p x = (p ^ x ^ end_tag, real (size x));
 
-fun free_or_skolem x =
+fun unless_skolem tag x =
   (case try Syntax.dest_skolem x of
-    None => tagit free_tag x
+    None => tagit tag x
   | Some x' => tagit skolem_tag x');
 
 in
@@ -56,9 +56,9 @@
   [("class", tagit tclass_tag),
    ("tfree", tagit tfree_tag),
    ("tvar", tagit tvar_tag),
-   ("free", free_or_skolem),
+   ("free", unless_skolem free_tag),
    ("bound", tagit bound_tag),
-   ("var", tagit var_tag)];
+   ("var", unless_skolem var_tag)];
 
 end;