diff -r 66aaa0eb9069 -r 0fce95478e19 lib/Tools/latex
--- a/lib/Tools/latex	Thu Jan 24 18:22:01 2002 +0100
+++ b/lib/Tools/latex	Thu Jan 24 22:41:44 2002 +0100
@@ -78,18 +78,7 @@
 function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
 function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
 function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
-
-function update_styles ()
-{
-  for NAME in "$ISABELLE_HOME/lib/texinputs"/*.sty
-  do
-    DEST="$DIR"/$(basename "$NAME")
-    if [ ! -e "$DEST" -o "$NAME" -nt "$DEST" ]; then
-      echo "updating $DEST"
-      cp -f "$NAME" "$DEST"
-    fi
-  done
-}
+function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
 
 case "$OUTFORMAT" in
   dvi)
@@ -132,7 +121,7 @@
     RC="$?"
     ;;
   sty)
-    update_styles
+    copy_styles
     RC="$?"
     ;;
   *)