# HG changeset patch
# User sultana
# Date 1333470802 -3600
# Node ID 15428dd82b54d9d5fcff92f92e96803477cb0ca6
# Parent  610d9c212376216d33df1355799155bf11bbe400
removed use of CharVector in generated parser, to make SMLNJ happy

diff -r 610d9c212376 -r 15428dd82b54 src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Tue Apr 03 17:33:22 2012 +0100
@@ -30,7 +30,9 @@
 
 for FILE in $INTERMEDIATE_FILES
 do
-  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE
+  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
+          -e 's/Unsafe\.(.*)/\1/g;' \
+          -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
 done
 ) > tptp_lexyacc.ML
 
diff -r 610d9c212376 -r 15428dd82b54 src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Tue Apr 03 17:48:16 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Tue Apr 03 17:33:22 2012 +0100
@@ -1342,9 +1342,9 @@
 		     yybl := size (!yyb);
 		     scan (s,AcceptingLeaves,l-i0,0))
 	    end
-	  else let val NewChar = Char.ord(CharVector.sub(!yyb,l))
+	  else let val NewChar = Char.ord(String.sub(!yyb,l))
 		val NewChar = if NewChar<128 then NewChar else 128
-		val NewState = Char.ord(CharVector.sub(trans,NewChar))
+		val NewState = Char.ord(String.sub(trans,NewChar))
 		in if NewState=0 then action(l,NewAcceptingLeaves)
 		else scan(NewState,NewAcceptingLeaves,l+1,i0)
 	end