diff -r 1cf20169660c -r 762a739c9eb4 Paper/ROOT.ML --- a/Paper/ROOT.ML Wed May 26 15:26:22 2010 +0200 +++ b/Paper/ROOT.ML Wed May 26 15:35:34 2010 +0200 @@ -1,3 +1,3 @@ quick_and_dirty := true; -no_document use_thys ["LaTeXsugar", "../Nominal/FSet"]; +no_document use_thys ["LaTeXsugar"]; use_thys ["Paper"]; \ No newline at end of file