# HG changeset patch
# User wenzelm
# Date 1376861858 -7200
# Node ID d815e25ead03cd636c1617b2002554f224d5a940
# Parent  ade63ccd6f4ed83f0225b005ce2a83cc462ef6e9
tuned;

diff -r ade63ccd6f4e -r d815e25ead03 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Aug 18 22:44:39 2013 +0200
+++ b/src/HOL/Word/Word.thy	Sun Aug 18 23:37:38 2013 +0200
@@ -4646,9 +4646,9 @@
 
 declare bin_to_bl_def [simp]
 
-ML_file "~~/src/HOL/Word/Tools/word_lib.ML"
-ML_file "~~/src/HOL/Word/Tools/smt_word.ML"
-setup {* SMT_Word.setup *}
+ML_file "Tools/word_lib.ML"
+ML_file "Tools/smt_word.ML"
+setup SMT_Word.setup
 
 hide_const (open) Word