# HG changeset patch
# User wenzelm
# Date 1492610038 -7200
# Node ID ffedb16f382f099f6a66efe50c940df47573a03c
# Parent  a72ab197e68134b4257c988c054c5d718e87adcc
clarified session structure: avoid ambiguity of file ~~/src/HOL/Library/Old_Datatype.thy;

diff -r a72ab197e681 -r ffedb16f382f src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Apr 19 12:27:36 2017 +0200
+++ b/src/HOL/ROOT	Wed Apr 19 15:53:58 2017 +0200
@@ -20,7 +20,8 @@
   *}
   options [document = false, theory_qualifier = "HOL",
     quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
-  theories "~~/src/HOL/Library/Old_Datatype"
+  sessions "HOL-Library"
+  theories "HOL-Library.Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"