# HG changeset patch
# User wenzelm
# Date 938257566 -7200
# Node ID 4fbdb8a0c3785ec358774fdadc38f6bdbc8f776b
# Parent  c97c3ad15d2eb2ecd8a7b25270057baec4a7581b
skolem_tag;

diff -r c97c3ad15d2e -r 4fbdb8a0c378 src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sat Sep 25 13:05:38 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sat Sep 25 13:06:06 1999 +0200
@@ -74,9 +74,15 @@
 val free_tag = oct_char "354";
 val bound_tag = oct_char "355";
 val var_tag = oct_char "356";
+val skolem_tag = oct_char "357";
 
 fun tagit p x = (p ^ x ^ end_tag, real (size x));
 
+fun free_or_skolem x =
+  (case try Syntax.dest_skolem x of
+    None => tagit free_tag x
+  | Some x' => tagit skolem_tag x');
+
 in
 
 val proof_general_trans =
@@ -84,7 +90,7 @@
   [("class", tagit tclass_tag),
    ("tfree", tagit tfree_tag),
    ("tvar", tagit tvar_tag),
-   ("free", tagit free_tag),
+   ("free", free_or_skolem),
    ("bound", tagit bound_tag),
    ("var", tagit var_tag)];