# HG changeset patch
# User haftmann
# Date 1330697885 -3600
# Node ID a65e18ceb1e3d98cecefa747ad4bb4053eeda2da
# Parent  aa9f5c3bcd4c99e641e092852fbb7743a004a3a0
tuned import

diff -r aa9f5c3bcd4c -r a65e18ceb1e3 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Fri Mar 02 15:17:54 2012 +0100
+++ b/src/HOL/Library/Reflection.thy	Fri Mar 02 15:18:05 2012 +0100
@@ -6,13 +6,13 @@
 
 theory Reflection
 imports Main
-uses "reify_data.ML" ("reflection.ML")
+uses
+  "~~/src/HOL/Library/reify_data.ML"
+  "~~/src/HOL/Library/reflection.ML"
 begin
 
 setup {* Reify_Data.setup *}
 
-use "reflection.ML"
-
 method_setup reify = {*
   Attrib.thms --
     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
@@ -41,3 +41,4 @@
 *}
 
 end
+