# HG changeset patch # User wenzelm # Date 968686758 -7200 # Node ID dab013ea6b6382803b92deffbc78cb6700ea14b8 # Parent 5af7632388a0d7f888880c70cca32aceb13dcaac proper markup of schematic (!) skolems; diff -r 5af7632388a0 -r dab013ea6b63 src/Pure/Interface/proof_general.ML --- 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;