token_trans: symbol length;

--- a/src/Pure/Interface/proof_general.ML	Thu Mar 02 18:18:59 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Fri Mar 03 01:58:57 2000 +0100
@@ -42,7 +42,7 @@
 val var_tag = oct_char "356";
 val skolem_tag = oct_char "357";
 
-fun tagit p x = (p ^ x ^ end_tag, real (size x));
+fun tagit p x = (p ^ x ^ end_tag, real (Symbol.length (Symbol.explode x)));
 
 fun unless_skolem tag x =
   (case try Syntax.dest_skolem x of