# HG changeset patch
# User wenzelm
# Date 952045137 -3600
# Node ID 057a3e303f380df1111d17c75da18728dc8cce39
# Parent  c411706dc50359e2b7f912f34c08b6b7a5e41ed3
token_trans: symbol length;

diff -r c411706dc503 -r 057a3e303f38 src/Pure/Interface/proof_general.ML
--- 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