# HG changeset patch
# User wenzelm
# Date 889456288 -3600
# Node ID 20ade76722d66a6a7e907196988f505865e4dd11
# Parent  fc5687450acc4ebed19b85cb0bf50720a866ebd5
read_var;

diff -r fc5687450acc -r 20ade76722d6 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Mar 09 16:11:13 1998 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Mar 09 16:11:28 1998 +0100
@@ -332,7 +332,7 @@
               raise exn));
 
     fun term_of (Constant a) = trans a []
-      | term_of (Variable x) = scan_var x
+      | term_of (Variable x) = read_var x
       | term_of (Appl (Constant a :: (asts as _ :: _))) =
           trans a (map term_of asts)
       | term_of (Appl (ast :: (asts as _ :: _))) =