src/Pure/Thy/present.ML
changeset 72635 2a329baa7d39
parent 72622 830222403681
child 72636 09ee9eb7a3d3
--- a/src/Pure/Thy/present.ML	Tue Nov 17 16:34:01 2020 +0100
+++ b/src/Pure/Thy/present.ML	Tue Nov 17 16:48:18 2020 +0100
@@ -42,9 +42,9 @@
     val link = html_name thy';
   in
     if session = session' then SOME link
-    else if chapter = chapter' then SOME (Path.parent + Path.basic session + link)
-    else if chapter = Context.PureN then NONE
-    else SOME (Path.parent + Path.parent + Path.basic chapter + Path.basic session + link)
+    else if chapter = chapter' then SOME (Path.parent + Path.basic session' + link)
+    else if chapter' = Context.PureN then NONE
+    else SOME (Path.parent + Path.parent + Path.basic chapter' + Path.basic session' + link)
   end;
 
 fun theory_document symbols A Bs body =