# HG changeset patch
# User wenzelm
# Date 1536917661 -7200
# Node ID 10da16970d82ed4f2b36df9ae811dba154ded7db
# Parent  e6678381151899a8e67b6ec6cded77a2176aca4e# Parent  d961e11e0e87f903da5f00c071fad579ff2fe83c
merged

diff -r e66783811518 -r 10da16970d82 src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Fri Sep 14 10:07:59 2018 +0200
+++ b/src/Pure/Tools/update_cartouches.scala	Fri Sep 14 11:34:21 2018 +0200
@@ -104,6 +104,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_cartouches(replace_text, Path.explode(File.standard_path(file)))
+      } update_cartouches(replace_text, File.path(file))
     })
 }
diff -r e66783811518 -r 10da16970d82 src/Pure/Tools/update_comments.scala
--- a/src/Pure/Tools/update_comments.scala	Fri Sep 14 10:07:59 2018 +0200
+++ b/src/Pure/Tools/update_comments.scala	Fri Sep 14 11:34:21 2018 +0200
@@ -63,6 +63,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_comments(Path.explode(File.standard_path(file)))
+      } update_comments(File.path(file))
     })
 }
diff -r e66783811518 -r 10da16970d82 src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Fri Sep 14 10:07:59 2018 +0200
+++ b/src/Pure/Tools/update_header.scala	Fri Sep 14 11:34:21 2018 +0200
@@ -56,6 +56,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_header(section, Path.explode(File.standard_path(file)))
+      } update_header(section, File.path(file))
     })
 }
diff -r e66783811518 -r 10da16970d82 src/Pure/Tools/update_then.scala
--- a/src/Pure/Tools/update_then.scala	Fri Sep 14 10:07:59 2018 +0200
+++ b/src/Pure/Tools/update_then.scala	Fri Sep 14 11:34:21 2018 +0200
@@ -50,6 +50,6 @@
       for {
         spec <- specs
         file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-      } update_then(Path.explode(File.standard_path(file)))
+      } update_then(File.path(file))
     })
 }
diff -r e66783811518 -r 10da16970d82 src/Pure/Tools/update_theorems.scala
--- a/src/Pure/Tools/update_theorems.scala	Fri Sep 14 10:07:59 2018 +0200
+++ b/src/Pure/Tools/update_theorems.scala	Fri Sep 14 11:34:21 2018 +0200
@@ -52,6 +52,6 @@
     for {
       spec <- specs
       file <- File.find_files(Path.explode(spec).file, file => file.getName.endsWith(".thy"))
-    } update_theorems(Path.explode(File.standard_path(file)))
+    } update_theorems(File.path(file))
   })
 }