diff --git a/Citadelle/ROOT b/Citadelle/ROOT
index 8e1d225ce4e3b808900dbae65bad3059934dbdc0..988554ce8e69542ae63f440e9d69a0380112ca5e 100644
--- a/Citadelle/ROOT
+++ b/Citadelle/ROOT
@@ -72,6 +72,9 @@ session FOCL in "src/uml_ocl" = "HOL-Library" +
   options [document=pdf,document_output=document_generated,
            document_variants="document=noexample,-afp,-annexa",
            show_question_marks = false]
+  sessions
+    OCL
+    Isabelle_Meta_Model
   theories
     UML_OCL
   document_files
diff --git a/Citadelle/examples/C_Model_core.thy b/Citadelle/examples/C_Model_core.thy
index b547e33bafbdb5de370a32a4291d7cff30d9ba3f..6a56654ffece890ad4f047cab32736d9b2dcfcf2 100644
--- a/Citadelle/examples/C_Model_core.thy
+++ b/Citadelle/examples/C_Model_core.thy
@@ -38,7 +38,7 @@
 
 theory C_Model_core
   imports "$HASKABELLE_HOME_USER/default/Prelude"
-          FOCL.UML_Main
+          OCL.UML_Main
           Citadelle.Generator_dynamic_concurrent
           Citadelle_C_init.C_Model_init
 begin
diff --git a/Citadelle/examples/C_Model_init.thy b/Citadelle/examples/C_Model_init.thy
index 2f90a2d035da61bf4c756ec7a2a60eb224159466..b39139d1cd9a64878c4e6e33e28226d70e2e44a3 100644
--- a/Citadelle/examples/C_Model_init.thy
+++ b/Citadelle/examples/C_Model_init.thy
@@ -37,7 +37,7 @@
  ******************************************************************************)
 
 theory C_Model_init
-  imports FOCL.Printer_init
+  imports Isabelle_Meta_Model.Printer_init
           Citadelle.Old_Datatype
 begin
 
diff --git a/Citadelle/src/compiler/Generator_dynamic_concurrent.thy b/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
index 4a0e939e8ba02998ef428fbf9f084536e29dee8b..508812a4714f14952fd163efd6771ed456e73b90 100644
--- a/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_concurrent.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
 
 theory Generator_dynamic_concurrent
 imports FOCL.Printer
-        FOCL.Isabelle_typedecl
+        Isabelle_Meta_Model.Isabelle_typedecl
         "~~/src/HOL/Library/Old_Datatype"
   keywords (* OCL (USE tool) *)
            "Between"
diff --git a/Citadelle/src/compiler/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
index 3bd4452f359a2bef472a7a8d3c09a0d5c19f53c9..0fadcb684a0eac6a538246b3336be37f0bc244fa 100644
--- a/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_export_testing.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
 
 theory Generator_dynamic_export_testing
 imports FOCL.Printer
-        FOCL.Isabelle_typedecl
+        Isabelle_Meta_Model.Isabelle_typedecl
         "~~/src/HOL/Library/Old_Datatype"
   keywords (* OCL (USE tool) *)
            "Between"
diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index ed31d334803863e591ef67b20d68f16e38962bd7..3bd69c83e8073ee7b8584f229c6e28bd5d486a90 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -43,7 +43,7 @@ section\<open>Dynamic Meta Embedding with Reflection\<close>
 
 theory Generator_dynamic_sequential
 imports Printer
-        "../compiler_generic/isabelle_home/src/Pure/Isar/Isabelle_typedecl"
+        Isabelle_Meta_Model.Isabelle_typedecl
   keywords (* OCL (USE tool) *)
            "Between"
            "Attributes" "Operations" "Constraints"
diff --git a/Citadelle/src/compiler/core/Core_init.thy b/Citadelle/src/compiler/core/Core_init.thy
index a5dc319fb74d3fbb91b52b1e5cbaacd576a49c59..581656eaa09f4a79162b3fb8b8398dc1e941e9e6 100644
--- a/Citadelle/src/compiler/core/Core_init.thy
+++ b/Citadelle/src/compiler/core/Core_init.thy
@@ -331,7 +331,7 @@ As general remark, all the future translating steps
 will extensively use Isabelle expressions,
 represented by its Meta-Model, for example lots of functions will use @{term "Term_app"}...
 So the overall can be simplified by the use of polymorphic cartouches.
-It looks feasible to add a new front-end for cartouches in @{theory "FOCL.Init"}
+It looks feasible to add a new front-end for cartouches in @{theory "Isabelle_Meta_Model.Init"}
 supporting the use of Isabelle syntax in cartouches,
 then we could obtain at the end a parsed Isabelle Meta-Model in Isabelle.\<close>
 
diff --git a/Citadelle/src/compiler/meta/Meta_HKB.thy b/Citadelle/src/compiler/meta/Meta_HKB.thy
index 607922de053e506c88c2626d66ac3ce315eafc22..b6396cd48ac8c228386005a277267b1f850e79a7 100644
--- a/Citadelle/src/compiler/meta/Meta_HKB.thy
+++ b/Citadelle/src/compiler/meta/Meta_HKB.thy
@@ -39,7 +39,7 @@
 section\<open>Isabelle Meta-Model aka. AST definition of Isabelle\<close>
 
 theory Meta_HKB
-imports "../../compiler_generic/Init"
+imports Isabelle_Meta_Model.Init
 begin
 
 section \<open>Miscellaneous\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_META.thy b/Citadelle/src/compiler/meta/Meta_META.thy
index 6a9a5ba4ce804bd5cb11e7308c9dfb68f3b626c8..e9711d823ef161196ab104c132e67d29e9ba717c 100644
--- a/Citadelle/src/compiler/meta/Meta_META.thy
+++ b/Citadelle/src/compiler/meta/Meta_META.thy
@@ -45,7 +45,7 @@ theory  Meta_META
 imports Meta_UML
         Meta_UML_extended
         Meta_HKB
-        "../../compiler_generic/meta_isabelle/Meta_Isabelle"
+        Isabelle_Meta_Model.Meta_Isabelle
 begin
 
 subsection\<open>A Basic Meta-Model\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_UML.thy b/Citadelle/src/compiler/meta/Meta_UML.thy
index ee8b3258d664f96af6bb69decc139bc667f15070..94ece8b657c8071ce52aeeae73e17ef05201eea0 100644
--- a/Citadelle/src/compiler/meta/Meta_UML.thy
+++ b/Citadelle/src/compiler/meta/Meta_UML.thy
@@ -42,8 +42,8 @@
 section\<open>OCL Meta-Model aka. AST definition of OCL (I)\<close>
 
 theory  Meta_UML
-imports "../../compiler_generic/meta_isabelle/Meta_Pure"
-        "../Init_rbt"
+imports Isabelle_Meta_Model.Meta_Pure
+        Isabelle_Meta_Model.Init_rbt
 begin
 
 subsection\<open>Type Definition\<close>
diff --git a/Citadelle/src/compiler/meta/Meta_UML_extended.thy b/Citadelle/src/compiler/meta/Meta_UML_extended.thy
index 2bd589496b9afe99e526cbaf5bcb5685dc7ab1bf..6c2f0674ee068ae66a238ad20f31963e2cb3f4b3 100644
--- a/Citadelle/src/compiler/meta/Meta_UML_extended.thy
+++ b/Citadelle/src/compiler/meta/Meta_UML_extended.thy
@@ -42,7 +42,7 @@
 section\<open>OCL Meta-Model aka. AST definition of OCL (II)\<close>
 
 theory  Meta_UML_extended
-imports "../../compiler_generic/Init"
+imports Isabelle_Meta_Model.Init
 begin
 
 subsection\<open>Type Definition\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_HKB.thy b/Citadelle/src/compiler/meta/Parser_HKB.thy
index fbd32ed750ab75961c33b483d7718ab4f7f999ec..31cf1943d6dadda8744db76a9ad3a564b02a5b32 100644
--- a/Citadelle/src/compiler/meta/Parser_HKB.thy
+++ b/Citadelle/src/compiler/meta/Parser_HKB.thy
@@ -39,7 +39,7 @@ section\<open>Instantiating the Parser of Haskabelle\<close>
 
 theory  Parser_HKB
 imports Meta_HKB
-        "../../compiler_generic/meta_isabelle/Parser_init"
+        Isabelle_Meta_Model.Parser_init
 begin
 
 subsection\<open>Main\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_META.thy b/Citadelle/src/compiler/meta/Parser_META.thy
index 5b1e9fc5edda16629b162bef203fc8c16d17fcc8..69fa97a586c4a5acb54c78bead3fdf2e8d1dfc1c 100644
--- a/Citadelle/src/compiler/meta/Parser_META.thy
+++ b/Citadelle/src/compiler/meta/Parser_META.thy
@@ -164,7 +164,7 @@ section\<open>Finalizing the Parser\<close>
 text\<open>It should be feasible to invent a meta-command (e.g., @{text "datatype'"})
 to automatically generate the previous recursors in @{text Parse}.
 
-Otherwise as an extra check, one can also overload polymorphic cartouches in @{theory FOCL.Init}
+Otherwise as an extra check, one can also overload polymorphic cartouches in @{theory Isabelle_Meta_Model.Init}
 to really check that all the given constructor exists at the time of editing
 (similarly as writing @{verbatim "@{term ...}"},
 when it is embedded in a @{verbatim "text"} command).\<close>
diff --git a/Citadelle/src/compiler/meta/Parser_UML.thy b/Citadelle/src/compiler/meta/Parser_UML.thy
index 0621e0f480d9742a1e06f19e4532a2174dfb3713..e7da7299512b05a5cca5098df8ad4a68a05e4eca 100644
--- a/Citadelle/src/compiler/meta/Parser_UML.thy
+++ b/Citadelle/src/compiler/meta/Parser_UML.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Parser of OCL (I)\<close>
 
 theory  Parser_UML
 imports Meta_UML
-        "../../compiler_generic/meta_isabelle/Parser_Pure"
+        Isabelle_Meta_Model.Parser_Pure
 begin
 
 subsection\<open>Building Recursors for Records\<close> (* NOTE part to be automated *)
diff --git a/Citadelle/src/compiler/meta/Parser_UML_extended.thy b/Citadelle/src/compiler/meta/Parser_UML_extended.thy
index 0b5fe8b9aaaaa90eac6c0c0b0b86239ac0fc6583..fbbad2e59558633478d11d91820b12b69ce47e44 100644
--- a/Citadelle/src/compiler/meta/Parser_UML_extended.thy
+++ b/Citadelle/src/compiler/meta/Parser_UML_extended.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Parser of OCL (II)\<close>
 
 theory  Parser_UML_extended
 imports Meta_UML_extended
-        "../../compiler_generic/meta_isabelle/Parser_init"
+        Isabelle_Meta_Model.Parser_init
 begin
 
 subsection\<open>Building Recursors for Records\<close> (* NOTE part to be automated *)
diff --git a/Citadelle/src/compiler/meta/Printer_META.thy b/Citadelle/src/compiler/meta/Printer_META.thy
index c0e6d9062bf77ef90b4255fc5399cd212d2a36a6..74af181fdd6568378db8a9165fe0183673638092 100644
--- a/Citadelle/src/compiler/meta/Printer_META.thy
+++ b/Citadelle/src/compiler/meta/Printer_META.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Printer for META\<close>
 
 theory  Printer_META
 imports Parser_META
-        "../../compiler_generic/meta_isabelle/Printer_Isabelle"
+        Isabelle_Meta_Model.Printer_Isabelle
         Printer_UML_extended
 begin
 
diff --git a/Citadelle/src/compiler/meta/Printer_UML.thy b/Citadelle/src/compiler/meta/Printer_UML.thy
index 39e9fffb29e18690e164d86479c58606220c596e..4346a73c24608b213811a5f2e879e3c80e63ea47 100644
--- a/Citadelle/src/compiler/meta/Printer_UML.thy
+++ b/Citadelle/src/compiler/meta/Printer_UML.thy
@@ -43,7 +43,7 @@ section\<open>Instantiating the Printer for OCL (I)\<close>
 
 theory  Printer_UML
 imports Meta_UML
-        "../../compiler_generic/meta_isabelle/Printer_Pure"
+        Isabelle_Meta_Model.Printer_Pure
 begin
 
 context Print
diff --git a/Citadelle/src/compiler_generic/ROOT b/Citadelle/src/compiler_generic/ROOT
index 8dd9c505ced21468a9f2939a8963972eb842e11b..aef7913c13104194eb65cb3d5995d0d0d60ef8d5 100644
--- a/Citadelle/src/compiler_generic/ROOT
+++ b/Citadelle/src/compiler_generic/ROOT
@@ -41,20 +41,6 @@
 
 chapter AFP
 
-session Meta_Isabelle (AFP) = "HOL-Library" +
-  description {* Meta_Isabelle *}
-  options [timeout = 600, document = pdf, document_output = document_generated]
-  theories [document = false]
-    "isabelle_home/src/HOL/ex/Isabelle_Cartouche_Examples"
-    "isabelle_home/src/Tools/Code/Isabelle_code_runtime"
-  theories
-    "meta_isabelle/Parser_Pure"
-    "meta_isabelle/Meta_Isabelle"
-    "meta_isabelle/Printer_Isabelle"
-  document_files
-    "root.bib"
-    "root.tex"
-
 session Isabelle_Meta_Model (AFP) = "HOL-Library" +
   description {* Isabelle_Meta_Model containing a Toy Example *}
   options [timeout = 600, document = pdf, document_output = document_generated]
@@ -83,23 +69,3 @@ session Isabelle_Meta_Model (AFP) = "HOL-Library" +
   document_files
     "root.bib"
     "root.tex"
-
-(*
-session Toy_All = "HOL-Library" +
-  description {* Toy_All *}
-  options [timeout = 600, document = pdf, document_output = document_generated]
-  theories [document = false]
-    "isabelle_home/src/HOL/ex/Isabelle_Cartouche_Examples"
-    "isabelle_home/src/Tools/Code/Isabelle_code_runtime"
-    "isabelle_home/src/Pure/Isar/Isabelle_typedecl"
-  theories
-    "toy_example/embedding/Generator_static"
-    (* "toy_example/embedding/Generator_dynamic_sequential" (* is imported by the following examples *) *)
-    "toy_example/generator/Design_deep"
-    "toy_example/generator/Design_shallow"
-    "toy_example/document_generated/Design_generated_generated"
-    "document/Rail"
-  document_files
-    "root.bib"
-    "root.tex"
-*)
diff --git a/Citadelle/src/uml_ocl/UML_OCL.thy b/Citadelle/src/uml_ocl/UML_OCL.thy
index 8449b51bcf32ba9ed040ef0a43f291416dd83785..6bb69dc2f933e44942e5eea8f8ea80f5a00bbb7e 100644
--- a/Citadelle/src/uml_ocl/UML_OCL.thy
+++ b/Citadelle/src/uml_ocl/UML_OCL.thy
@@ -44,7 +44,7 @@
  ******************************************************************************)
 
 theory   UML_OCL
-imports  "../uml_main/UML_Main"
+imports  OCL.UML_Main
          "../../examples/archive/Monads" (* NOTE: perform lazily the extraction of generation_syntax
                                             so that dependencies can alternate among theories *)
          "../compiler/Static"