--- 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)];