src/HOL/ROOT

--- a/src/HOL/ROOT	Wed Feb 19 22:05:15 2014 +0100
+++ b/src/HOL/ROOT	Wed Feb 19 22:08:47 2014 +0100
@@ -111,7 +111,7 @@
 session "HOL-IMP" in IMP = HOL +
   options [document_graph, document_variants=document]
   theories [document = false]
-    "~~/src/HOL/ex/Interpretation_with_Defs"
+    "~~/src/Tools/Permanent_Interpretation"
     "~~/src/HOL/Library/While_Combinator"
     "~~/src/HOL/Library/Char_ord"
     "~~/src/HOL/Library/List_lexord"