--- a/src/Pure/Interface/proof_general.ML Mon Sep 11 17:37:50 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML Mon Sep 11 17:39:18 2000 +0200
@@ -45,11 +45,19 @@
fun tagit p x = (p ^ x ^ end_tag, real (Symbol.length (Symbol.explode x)));
-fun unless_skolem tag x =
+fun free_or_skolem x =
(case try Syntax.dest_skolem x of
- None => tagit tag x
+ None => tagit free_tag x
| Some x' => tagit skolem_tag x');
+fun var_or_skolem s =
+ (case Syntax.read_var s of
+ Var ((x, i), _) =>
+ (case try Syntax.dest_skolem x of
+ None => tagit var_tag s
+ | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
+ | _ => tagit var_tag s);
+
in
val proof_general_trans =
@@ -57,9 +65,9 @@
[("class", tagit tclass_tag),
("tfree", tagit tfree_tag),
("tvar", tagit tvar_tag),
- ("free", unless_skolem free_tag),
+ ("free", free_or_skolem),
("bound", tagit bound_tag),
- ("var", unless_skolem var_tag)];
+ ("var", var_or_skolem)];
end;