skolem_tag;
authorwenzelm
Sat Sep 25 13:06:06 1999 +0200 (1999-09-25 ago)
changeset 75974fbdb8a0c378
parent 7596 c97c3ad15d2e
child 7598 af320257c902
skolem_tag;
src/Pure/Interface/proof_general.ML
     1.1 --- a/src/Pure/Interface/proof_general.ML	Sat Sep 25 13:05:38 1999 +0200
     1.2 +++ b/src/Pure/Interface/proof_general.ML	Sat Sep 25 13:06:06 1999 +0200
     1.3 @@ -74,9 +74,15 @@
     1.4  val free_tag = oct_char "354";
     1.5  val bound_tag = oct_char "355";
     1.6  val var_tag = oct_char "356";
     1.7 +val skolem_tag = oct_char "357";
     1.8  
     1.9  fun tagit p x = (p ^ x ^ end_tag, real (size x));
    1.10  
    1.11 +fun free_or_skolem x =
    1.12 +  (case try Syntax.dest_skolem x of
    1.13 +    None => tagit free_tag x
    1.14 +  | Some x' => tagit skolem_tag x');
    1.15 +
    1.16  in
    1.17  
    1.18  val proof_general_trans =
    1.19 @@ -84,7 +90,7 @@
    1.20    [("class", tagit tclass_tag),
    1.21     ("tfree", tagit tfree_tag),
    1.22     ("tvar", tagit tvar_tag),
    1.23 -   ("free", tagit free_tag),
    1.24 +   ("free", free_or_skolem),
    1.25     ("bound", tagit bound_tag),
    1.26     ("var", tagit var_tag)];
    1.27