# HG changeset patch
# User wenzelm
# Date 889456086 -3600
# Node ID b159f5d98ceb1752898cc8f84828a4f388732fc1
# Parent  8459cf322011c6ff616e5ff73bd9bd7476ec834c
Syntax.indexname;

diff -r 8459cf322011 -r b159f5d98ceb src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Mar 09 16:07:22 1998 +0100
+++ b/src/Pure/drule.ML	Mon Mar 09 16:08:06 1998 +0100
@@ -114,9 +114,6 @@
 
 (** reading of instantiations **)
 
-fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
-        | _ => error("Lexical error in variable name " ^ quote (implode cs));
-
 fun absent ixn =
   error("No such variable in term: " ^ Syntax.string_of_vname ixn);
 
@@ -126,9 +123,9 @@
 fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
 let val {tsig,...} = Sign.rep_sg sign
     fun split([],tvs,vs) = (tvs,vs)
-      | split((sv,st)::l,tvs,vs) = (case explode sv of
-                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
-                | cs => split(l,tvs,(indexname cs,st)::vs));
+      | split((sv,st)::l,tvs,vs) = (case Symbol.explode sv of
+                  "'"::cs => split(l,(Syntax.indexname cs,st)::tvs,vs)
+                | cs => split(l,tvs,(Syntax.indexname cs,st)::vs));
     val (tvs,vs) = split(insts,[],[]);
     fun readT((a,i),st) =
         let val ixn = ("'" ^ a,i);