From 6cc76c9d2640cc0d690b52a12d00cd1e01822840 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Thu, 20 Jun 2019 19:53:59 +0200
Subject: [PATCH] workaround on local comment bug

---
 ontologies/Conceptual.thy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy
index 0872827a..4b7d21c9 100644
--- a/ontologies/Conceptual.thy
+++ b/ontologies/Conceptual.thy
@@ -54,11 +54,11 @@ ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
 ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
 *)
 
-section* [ test :: A ] \<open> Test and Validation\<close>
+section*[test::A]\<open>Test and Validation\<close>
 text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
-text* [ sdf  ] \<open> f @{thm refl}\<close> 
-text* [ sdfg ] \<open> fg @{thm refl}\<close>  
-text* [ xxxy ] \<open> dd @{docitem \<open>sdfg\<close>}  @{thm refl}\<close>  
+text*[sdf]\<open> f @{thm refl}\<close> 
+text*[ sdfg] \<open> fg @{thm refl}\<close>  
+text*[ xxxy ] \<open> dd @{docitem \<open>sdfg\<close>}  @{thm refl}\<close>  
 
 
 end