# HG changeset patch
# User paulson
# Date 846859360 -3600
# Node ID 0007679951438fe7a478905e55a4006af7962505
# Parent  084218afaf4b8266ac8dc640181ea7d421bfebdc
Changes tabs found in .thy files to spaces

diff -r 084218afaf4b -r 000767995143 src/Pure/Thy/thy_scan.ML
--- a/src/Pure/Thy/thy_scan.ML	Fri Nov 01 15:41:09 1996 +0100
+++ b/src/Pure/Thy/thy_scan.ML	Fri Nov 01 15:42:40 1996 +0100
@@ -75,6 +75,7 @@
       | (Some s, cs') => cons_fst ("\\" ^ s) (string cs' (inc_line n s)))
   | string (c :: cs) n = 
       if c = "\n" then string cs (n+1)
+      else if is_blank c then cons_fst " " (string cs n)
       else cons_fst c (string cs n)
   | string [] n = lex_err n "missing quote at end of string";