From f2a8c3e07e91ba9b2753d34f4294f6f1e8b47d58 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Tue, 12 Jun 2018 18:30:47 +0200
Subject: [PATCH] c-parser: session qualified imports for parser tests

---
 tools/c-parser/testfiles/ARM/asm_stmt.thy                 | 2 +-
 tools/c-parser/testfiles/ARM/imports/MachineWords.thy     | 2 +-
 tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy             | 2 +-
 tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy | 2 +-
 tools/c-parser/testfiles/X64/imports/MachineWords.thy     | 2 +-
 tools/c-parser/testfiles/analsignedoverflow.thy           | 2 +-
 tools/c-parser/testfiles/array_of_ptr.thy                 | 2 +-
 tools/c-parser/testfiles/arrays.thy                       | 2 +-
 tools/c-parser/testfiles/basic_char.thy                   | 2 +-
 tools/c-parser/testfiles/bigstruct.thy                    | 2 +-
 tools/c-parser/testfiles/breakcontinue.thy                | 2 +-
 tools/c-parser/testfiles/bug20060707.thy                  | 2 +-
 tools/c-parser/testfiles/bug_mvt20110302.thy              | 2 +-
 tools/c-parser/testfiles/bugzilla180.thy                  | 2 +-
 tools/c-parser/testfiles/bugzilla181.thy                  | 2 +-
 tools/c-parser/testfiles/bugzilla182.thy                  | 2 +-
 tools/c-parser/testfiles/builtins.thy                     | 2 +-
 tools/c-parser/testfiles/charlit.thy                      | 2 +-
 tools/c-parser/testfiles/codetests.thy                    | 2 +-
 tools/c-parser/testfiles/dc_20081211.thy                  | 2 +-
 tools/c-parser/testfiles/dc_embbug.thy                    | 2 +-
 tools/c-parser/testfiles/decl_only.thy                    | 2 +-
 tools/c-parser/testfiles/dont_translate.thy               | 2 +-
 tools/c-parser/testfiles/dupthms.thy                      | 2 +-
 tools/c-parser/testfiles/emptystmt.thy                    | 2 +-
 tools/c-parser/testfiles/errors/addrlocal.thy             | 2 +-
 tools/c-parser/testfiles/extern_builtin.thy               | 2 +-
 tools/c-parser/testfiles/extern_dups.thy                  | 2 +-
 tools/c-parser/testfiles/factorial.thy                    | 2 +-
 tools/c-parser/testfiles/fncall.thy                       | 2 +-
 tools/c-parser/testfiles/fnptr.thy                        | 2 +-
 tools/c-parser/testfiles/gcc_attribs.thy                  | 2 +-
 tools/c-parser/testfiles/ghoststate1.thy                  | 2 +-
 tools/c-parser/testfiles/ghoststate2.thy                  | 2 +-
 tools/c-parser/testfiles/globals_fn.thy                   | 2 +-
 tools/c-parser/testfiles/globals_in_record.thy            | 2 +-
 tools/c-parser/testfiles/globinits.thy                    | 2 +-
 tools/c-parser/testfiles/globsall_addressed.thy.broken    | 2 +-
 tools/c-parser/testfiles/guard_while.thy                  | 2 +-
 tools/c-parser/testfiles/hexliteral.thy                   | 2 +-
 tools/c-parser/testfiles/includes/test_locality.thy       | 2 +-
 tools/c-parser/testfiles/initialised_decls.thy            | 2 +-
 tools/c-parser/testfiles/inner_fncalls.thy                | 2 +-
 tools/c-parser/testfiles/int_promotion.thy                | 2 +-
 tools/c-parser/testfiles/isa2014.thy                      | 2 +-
 tools/c-parser/testfiles/jiraver039.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver092.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver105.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver110.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver150.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver224.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver253.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver254.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver307.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver310.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver313.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver315.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver332.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver336.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver337.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver344.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver345.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver384.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver400.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver422.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver426.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver429.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver432.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver434.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver439.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver440.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver443.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver443a.thy                  | 2 +-
 tools/c-parser/testfiles/jiraver456.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver464.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver473.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver54.thy                    | 2 +-
 tools/c-parser/testfiles/jiraver550.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver808.thy                   | 2 +-
 tools/c-parser/testfiles/jiraver881.thy                   | 2 +-
 tools/c-parser/testfiles/kmalloc.thy                      | 2 +-
 tools/c-parser/testfiles/list_reverse.thy                 | 2 +-
 tools/c-parser/testfiles/list_reverse_norm.thy            | 2 +-
 tools/c-parser/testfiles/locvarfncall.thy                 | 2 +-
 tools/c-parser/testfiles/longlong.thy                     | 2 +-
 tools/c-parser/testfiles/many_local_vars.thy              | 2 +-
 tools/c-parser/testfiles/modifies_assumptions.thy         | 2 +-
 tools/c-parser/testfiles/modifies_speed.thy               | 2 +-
 tools/c-parser/testfiles/multi_deref.thy                  | 2 +-
 tools/c-parser/testfiles/multidim_arrays.thy              | 2 +-
 tools/c-parser/testfiles/mutrec_modifies.thy              | 2 +-
 tools/c-parser/testfiles/parse_addr.thy                   | 2 +-
 tools/c-parser/testfiles/parse_c99block.thy               | 2 +-
 tools/c-parser/testfiles/parse_complit.thy                | 2 +-
 tools/c-parser/testfiles/parse_dowhile.thy                | 2 +-
 tools/c-parser/testfiles/parse_enum.thy                   | 2 +-
 tools/c-parser/testfiles/parse_fncall.thy                 | 2 +-
 tools/c-parser/testfiles/parse_forloop.thy                | 2 +-
 tools/c-parser/testfiles/parse_include.thy                | 2 +-
 tools/c-parser/testfiles/parse_protos.thy                 | 2 +-
 tools/c-parser/testfiles/parse_retfncall.thy              | 2 +-
 tools/c-parser/testfiles/parse_sizeof.thy                 | 2 +-
 tools/c-parser/testfiles/parse_someops.thy                | 2 +-
 tools/c-parser/testfiles/parse_spec.thy.broken            | 2 +-
 tools/c-parser/testfiles/parse_struct.thy                 | 2 +-
 tools/c-parser/testfiles/parse_struct_array.thy           | 2 +-
 tools/c-parser/testfiles/parse_switch.thy                 | 2 +-
 tools/c-parser/testfiles/parse_typecast.thy               | 2 +-
 tools/c-parser/testfiles/parse_voidfn.thy                 | 2 +-
 tools/c-parser/testfiles/phantom_mstate.thy               | 2 +-
 tools/c-parser/testfiles/populate_globals.thy             | 2 +-
 tools/c-parser/testfiles/postfixOps.thy                   | 2 +-
 tools/c-parser/testfiles/protoparamshadow.thy             | 2 +-
 tools/c-parser/testfiles/ptr_auxupd.thy                   | 2 +-
 tools/c-parser/testfiles/ptr_diff.thy                     | 2 +-
 tools/c-parser/testfiles/ptr_modifies.thy                 | 2 +-
 tools/c-parser/testfiles/ptr_umm.thy.broken               | 2 +-
 tools/c-parser/testfiles/really_simple.thy                | 2 +-
 tools/c-parser/testfiles/relspec.thy                      | 2 +-
 tools/c-parser/testfiles/retprefix.thy                    | 2 +-
 tools/c-parser/testfiles/selection_sort.thy               | 2 +-
 tools/c-parser/testfiles/shortcircuit.thy                 | 2 +-
 tools/c-parser/testfiles/signed_div.thy                   | 2 +-
 tools/c-parser/testfiles/signedoverflow.thy               | 2 +-
 tools/c-parser/testfiles/simple_annotated_fn.thy          | 2 +-
 tools/c-parser/testfiles/simple_constexpr_sizeof.thy      | 2 +-
 tools/c-parser/testfiles/simple_fn.thy                    | 2 +-
 tools/c-parser/testfiles/sizeof_typedef.thy               | 2 +-
 tools/c-parser/testfiles/spec_annotated_fn.thy            | 2 +-
 tools/c-parser/testfiles/spec_annotated_voidfn.thy        | 2 +-
 tools/c-parser/testfiles/swap.thy                         | 2 +-
 tools/c-parser/testfiles/switch_unsigned_signed.thy       | 2 +-
 tools/c-parser/testfiles/test_shifts.thy                  | 2 +-
 tools/c-parser/testfiles/ummbug20100217.thy               | 2 +-
 tools/c-parser/testfiles/untouched_globals.thy            | 2 +-
 tools/c-parser/testfiles/variable_munge.thy               | 2 +-
 tools/c-parser/testfiles/varinit.thy                      | 2 +-
 tools/c-parser/testfiles/void_ptr_init.thy                | 2 +-
 tools/c-parser/testfiles/volatile_asm.thy                 | 2 +-
 139 files changed, 139 insertions(+), 139 deletions(-)

diff --git a/tools/c-parser/testfiles/ARM/asm_stmt.thy b/tools/c-parser/testfiles/ARM/asm_stmt.thy
index 918248ee4..544a28da5 100644
--- a/tools/c-parser/testfiles/ARM/asm_stmt.thy
+++ b/tools/c-parser/testfiles/ARM/asm_stmt.thy
@@ -10,7 +10,7 @@
 
 theory asm_stmt
 
-imports "../../CTranslation"
+imports "CParser.CTranslation"
 
 begin
 
diff --git a/tools/c-parser/testfiles/ARM/imports/MachineWords.thy b/tools/c-parser/testfiles/ARM/imports/MachineWords.thy
index 0376dad99..7a55e0515 100644
--- a/tools/c-parser/testfiles/ARM/imports/MachineWords.thy
+++ b/tools/c-parser/testfiles/ARM/imports/MachineWords.thy
@@ -9,7 +9,7 @@
  *)
 
 theory MachineWords
-imports "../../../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 type_synonym machine_word_len = "32"
diff --git a/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy b/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
index 918248ee4..544a28da5 100644
--- a/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
+++ b/tools/c-parser/testfiles/ARM_HYP/asm_stmt.thy
@@ -10,7 +10,7 @@
 
 theory asm_stmt
 
-imports "../../CTranslation"
+imports "CParser.CTranslation"
 
 begin
 
diff --git a/tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy b/tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy
index 0376dad99..7a55e0515 100644
--- a/tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy
+++ b/tools/c-parser/testfiles/ARM_HYP/imports/MachineWords.thy
@@ -9,7 +9,7 @@
  *)
 
 theory MachineWords
-imports "../../../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 type_synonym machine_word_len = "32"
diff --git a/tools/c-parser/testfiles/X64/imports/MachineWords.thy b/tools/c-parser/testfiles/X64/imports/MachineWords.thy
index c86f9a1c5..61ced4c05 100644
--- a/tools/c-parser/testfiles/X64/imports/MachineWords.thy
+++ b/tools/c-parser/testfiles/X64/imports/MachineWords.thy
@@ -9,7 +9,7 @@
  *)
 
 theory MachineWords
-imports "../../../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 type_synonym machine_word_len = "64"
diff --git a/tools/c-parser/testfiles/analsignedoverflow.thy b/tools/c-parser/testfiles/analsignedoverflow.thy
index 1d4ebdb47..4ace450a0 100644
--- a/tools/c-parser/testfiles/analsignedoverflow.thy
+++ b/tools/c-parser/testfiles/analsignedoverflow.thy
@@ -9,7 +9,7 @@
  *)
 
 theory analsignedoverflow
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare [[anal_integer_conversion=true]]
diff --git a/tools/c-parser/testfiles/array_of_ptr.thy b/tools/c-parser/testfiles/array_of_ptr.thy
index 9700552ab..14a9d1e74 100644
--- a/tools/c-parser/testfiles/array_of_ptr.thy
+++ b/tools/c-parser/testfiles/array_of_ptr.thy
@@ -9,7 +9,7 @@
  *)
 
 theory array_of_ptr
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "array_of_ptr.c"
diff --git a/tools/c-parser/testfiles/arrays.thy b/tools/c-parser/testfiles/arrays.thy
index b811e1f34..2a8e7680d 100644
--- a/tools/c-parser/testfiles/arrays.thy
+++ b/tools/c-parser/testfiles/arrays.thy
@@ -9,7 +9,7 @@
  *)
 
 theory arrays
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "arrays.c"
diff --git a/tools/c-parser/testfiles/basic_char.thy b/tools/c-parser/testfiles/basic_char.thy
index fee51d656..e0e88779a 100644
--- a/tools/c-parser/testfiles/basic_char.thy
+++ b/tools/c-parser/testfiles/basic_char.thy
@@ -9,7 +9,7 @@
  *)
 
 theory basic_char
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "basic_char.c"
diff --git a/tools/c-parser/testfiles/bigstruct.thy b/tools/c-parser/testfiles/bigstruct.thy
index 853d1902e..fb335de32 100644
--- a/tools/c-parser/testfiles/bigstruct.thy
+++ b/tools/c-parser/testfiles/bigstruct.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bigstruct
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bigstruct.c"
diff --git a/tools/c-parser/testfiles/breakcontinue.thy b/tools/c-parser/testfiles/breakcontinue.thy
index 0f7dc451c..e74ebc48c 100644
--- a/tools/c-parser/testfiles/breakcontinue.thy
+++ b/tools/c-parser/testfiles/breakcontinue.thy
@@ -9,7 +9,7 @@
  *)
 
 theory breakcontinue
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare sep_conj_ac [simp add]
diff --git a/tools/c-parser/testfiles/bug20060707.thy b/tools/c-parser/testfiles/bug20060707.thy
index b49ba7311..6dcd377f4 100644
--- a/tools/c-parser/testfiles/bug20060707.thy
+++ b/tools/c-parser/testfiles/bug20060707.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bug20060707
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bug20060707.c"
diff --git a/tools/c-parser/testfiles/bug_mvt20110302.thy b/tools/c-parser/testfiles/bug_mvt20110302.thy
index e00eda07b..e64fefa6c 100644
--- a/tools/c-parser/testfiles/bug_mvt20110302.thy
+++ b/tools/c-parser/testfiles/bug_mvt20110302.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bug_mvt20110302
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bug_mvt20110302.c"
diff --git a/tools/c-parser/testfiles/bugzilla180.thy b/tools/c-parser/testfiles/bugzilla180.thy
index 1e6a9a5c1..10bbee01a 100644
--- a/tools/c-parser/testfiles/bugzilla180.thy
+++ b/tools/c-parser/testfiles/bugzilla180.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bugzilla180
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bugzilla180.c"
diff --git a/tools/c-parser/testfiles/bugzilla181.thy b/tools/c-parser/testfiles/bugzilla181.thy
index 1d13ba901..8c9b4eef0 100644
--- a/tools/c-parser/testfiles/bugzilla181.thy
+++ b/tools/c-parser/testfiles/bugzilla181.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bugzilla181
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bugzilla181.c"
diff --git a/tools/c-parser/testfiles/bugzilla182.thy b/tools/c-parser/testfiles/bugzilla182.thy
index e104323de..fcbf3cc92 100644
--- a/tools/c-parser/testfiles/bugzilla182.thy
+++ b/tools/c-parser/testfiles/bugzilla182.thy
@@ -9,7 +9,7 @@
  *)
 
 theory bugzilla182
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "bugzilla182.c"
diff --git a/tools/c-parser/testfiles/builtins.thy b/tools/c-parser/testfiles/builtins.thy
index 8ba209c5b..b0ceb73bc 100644
--- a/tools/c-parser/testfiles/builtins.thy
+++ b/tools/c-parser/testfiles/builtins.thy
@@ -9,7 +9,7 @@
  *)
 
 theory builtins
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "builtins.c"
diff --git a/tools/c-parser/testfiles/charlit.thy b/tools/c-parser/testfiles/charlit.thy
index 8d42b2921..8a56bb471 100644
--- a/tools/c-parser/testfiles/charlit.thy
+++ b/tools/c-parser/testfiles/charlit.thy
@@ -9,7 +9,7 @@
  *)
 
 theory charlit
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "charlit.c"
diff --git a/tools/c-parser/testfiles/codetests.thy b/tools/c-parser/testfiles/codetests.thy
index afb7cc4a7..7fbcff8d1 100644
--- a/tools/c-parser/testfiles/codetests.thy
+++ b/tools/c-parser/testfiles/codetests.thy
@@ -9,7 +9,7 @@
  *)
 
 theory codetests
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 ML {* Context.>> (Context.map_theory (
diff --git a/tools/c-parser/testfiles/dc_20081211.thy b/tools/c-parser/testfiles/dc_20081211.thy
index fbf3a22d2..a54f2703d 100644
--- a/tools/c-parser/testfiles/dc_20081211.thy
+++ b/tools/c-parser/testfiles/dc_20081211.thy
@@ -9,7 +9,7 @@
  *)
 
 theory dc_20081211
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "dc_20081211.c"
diff --git a/tools/c-parser/testfiles/dc_embbug.thy b/tools/c-parser/testfiles/dc_embbug.thy
index 2c8f38c7e..64a3d24e1 100644
--- a/tools/c-parser/testfiles/dc_embbug.thy
+++ b/tools/c-parser/testfiles/dc_embbug.thy
@@ -9,7 +9,7 @@
  *)
 
 theory dc_embbug
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "dc_embbug.c"
diff --git a/tools/c-parser/testfiles/decl_only.thy b/tools/c-parser/testfiles/decl_only.thy
index d27f1bcac..8f29f7984 100644
--- a/tools/c-parser/testfiles/decl_only.thy
+++ b/tools/c-parser/testfiles/decl_only.thy
@@ -9,7 +9,7 @@
  *)
 
 theory decl_only
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "decl_only.c"
diff --git a/tools/c-parser/testfiles/dont_translate.thy b/tools/c-parser/testfiles/dont_translate.thy
index 458138097..f29165046 100644
--- a/tools/c-parser/testfiles/dont_translate.thy
+++ b/tools/c-parser/testfiles/dont_translate.thy
@@ -9,7 +9,7 @@
  *)
 
 theory dont_translate
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "dont_translate.c"
diff --git a/tools/c-parser/testfiles/dupthms.thy b/tools/c-parser/testfiles/dupthms.thy
index 5758362b6..c3c23ebbd 100644
--- a/tools/c-parser/testfiles/dupthms.thy
+++ b/tools/c-parser/testfiles/dupthms.thy
@@ -9,7 +9,7 @@
  *)
 
 theory dupthms
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "dupthms.c"
diff --git a/tools/c-parser/testfiles/emptystmt.thy b/tools/c-parser/testfiles/emptystmt.thy
index b03ed6637..02b3a44fa 100644
--- a/tools/c-parser/testfiles/emptystmt.thy
+++ b/tools/c-parser/testfiles/emptystmt.thy
@@ -9,7 +9,7 @@
  *)
 
 theory emptystmt
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "emptystmt.c"
diff --git a/tools/c-parser/testfiles/errors/addrlocal.thy b/tools/c-parser/testfiles/errors/addrlocal.thy
index c4b3fd5df..46fa6d470 100644
--- a/tools/c-parser/testfiles/errors/addrlocal.thy
+++ b/tools/c-parser/testfiles/errors/addrlocal.thy
@@ -9,7 +9,7 @@
  *)
 
 theory addrlocal
-imports "../../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "addrlocal.c";
diff --git a/tools/c-parser/testfiles/extern_builtin.thy b/tools/c-parser/testfiles/extern_builtin.thy
index 5d4bb8eee..6de631b6f 100644
--- a/tools/c-parser/testfiles/extern_builtin.thy
+++ b/tools/c-parser/testfiles/extern_builtin.thy
@@ -9,7 +9,7 @@
  *)
 
 theory extern_builtin
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 declare [[allow_underscore_idents=true]]
diff --git a/tools/c-parser/testfiles/extern_dups.thy b/tools/c-parser/testfiles/extern_dups.thy
index 892fe35a8..b19fd99a4 100644
--- a/tools/c-parser/testfiles/extern_dups.thy
+++ b/tools/c-parser/testfiles/extern_dups.thy
@@ -9,7 +9,7 @@
  *)
 
 theory extern_dups
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "extern_dups.c"
diff --git a/tools/c-parser/testfiles/factorial.thy b/tools/c-parser/testfiles/factorial.thy
index 97f3d7220..eb31ea623 100644
--- a/tools/c-parser/testfiles/factorial.thy
+++ b/tools/c-parser/testfiles/factorial.thy
@@ -9,7 +9,7 @@
  *)
 
 theory factorial
-imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
+imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
 begin
 
 declare hrs_simps [simp add]
diff --git a/tools/c-parser/testfiles/fncall.thy b/tools/c-parser/testfiles/fncall.thy
index b07f369b8..ad46ed9ff 100644
--- a/tools/c-parser/testfiles/fncall.thy
+++ b/tools/c-parser/testfiles/fncall.thy
@@ -9,7 +9,7 @@
  *)
 
 theory fncall
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare sep_conj_ac [simp add]
diff --git a/tools/c-parser/testfiles/fnptr.thy b/tools/c-parser/testfiles/fnptr.thy
index 45afaebdd..a26a74520 100644
--- a/tools/c-parser/testfiles/fnptr.thy
+++ b/tools/c-parser/testfiles/fnptr.thy
@@ -9,7 +9,7 @@
  *)
 
 theory fnptr
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 ML {*
diff --git a/tools/c-parser/testfiles/gcc_attribs.thy b/tools/c-parser/testfiles/gcc_attribs.thy
index ffaa54d0e..4f83930d1 100644
--- a/tools/c-parser/testfiles/gcc_attribs.thy
+++ b/tools/c-parser/testfiles/gcc_attribs.thy
@@ -9,7 +9,7 @@
  *)
 
 theory gcc_attribs
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "gcc_attribs.c"
diff --git a/tools/c-parser/testfiles/ghoststate1.thy b/tools/c-parser/testfiles/ghoststate1.thy
index 7b3b15f2a..79ae4d20e 100644
--- a/tools/c-parser/testfiles/ghoststate1.thy
+++ b/tools/c-parser/testfiles/ghoststate1.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ghoststate1
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "simple_annotated_fn.c" [ghostty="nat \<Rightarrow> nat"]
diff --git a/tools/c-parser/testfiles/ghoststate2.thy b/tools/c-parser/testfiles/ghoststate2.thy
index 3fefeb686..b062cfe35 100644
--- a/tools/c-parser/testfiles/ghoststate2.thy
+++ b/tools/c-parser/testfiles/ghoststate2.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ghoststate2
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 (*
diff --git a/tools/c-parser/testfiles/globals_fn.thy b/tools/c-parser/testfiles/globals_fn.thy
index 670ef239a..5117ad4e4 100644
--- a/tools/c-parser/testfiles/globals_fn.thy
+++ b/tools/c-parser/testfiles/globals_fn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory globals_fn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "globals_fn.c"
diff --git a/tools/c-parser/testfiles/globals_in_record.thy b/tools/c-parser/testfiles/globals_in_record.thy
index e9dcba228..4cfcc4b70 100644
--- a/tools/c-parser/testfiles/globals_in_record.thy
+++ b/tools/c-parser/testfiles/globals_in_record.thy
@@ -10,7 +10,7 @@
 
 theory globals_in_record
 imports
-  "../CTranslation"
+  "CParser.CTranslation"
 begin
 
 install_C_file "globals_in_record.c"
diff --git a/tools/c-parser/testfiles/globinits.thy b/tools/c-parser/testfiles/globinits.thy
index fa5069d8c..a85789d81 100644
--- a/tools/c-parser/testfiles/globinits.thy
+++ b/tools/c-parser/testfiles/globinits.thy
@@ -9,7 +9,7 @@
  *)
 
 theory globinits
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "globinits.c"
diff --git a/tools/c-parser/testfiles/globsall_addressed.thy.broken b/tools/c-parser/testfiles/globsall_addressed.thy.broken
index e481ce880..87020a98e 100644
--- a/tools/c-parser/testfiles/globsall_addressed.thy.broken
+++ b/tools/c-parser/testfiles/globsall_addressed.thy.broken
@@ -8,7 +8,7 @@
  * @TAG(NICTA_BSD)
  *)
 theory globsall_addressed
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   declare [[globals_all_addressed=true]]
diff --git a/tools/c-parser/testfiles/guard_while.thy b/tools/c-parser/testfiles/guard_while.thy
index 990d7157e..f9e5840f0 100644
--- a/tools/c-parser/testfiles/guard_while.thy
+++ b/tools/c-parser/testfiles/guard_while.thy
@@ -9,7 +9,7 @@
  *)
 
 theory guard_while
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "guard_while.c"
diff --git a/tools/c-parser/testfiles/hexliteral.thy b/tools/c-parser/testfiles/hexliteral.thy
index b012f98cd..945c62c27 100644
--- a/tools/c-parser/testfiles/hexliteral.thy
+++ b/tools/c-parser/testfiles/hexliteral.thy
@@ -9,7 +9,7 @@
  *)
 
 theory hexliteral
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "hexliteral.c"
diff --git a/tools/c-parser/testfiles/includes/test_locality.thy b/tools/c-parser/testfiles/includes/test_locality.thy
index cf89600f1..68799428f 100644
--- a/tools/c-parser/testfiles/includes/test_locality.thy
+++ b/tools/c-parser/testfiles/includes/test_locality.thy
@@ -9,7 +9,7 @@
  *)
 
 theory test_locality
-imports "../../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "test_include2.h"
diff --git a/tools/c-parser/testfiles/initialised_decls.thy b/tools/c-parser/testfiles/initialised_decls.thy
index 4541bb91d..71efd1d8e 100644
--- a/tools/c-parser/testfiles/initialised_decls.thy
+++ b/tools/c-parser/testfiles/initialised_decls.thy
@@ -9,7 +9,7 @@
  *)
 
 theory initialised_decls
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "initialised_decls.c"
diff --git a/tools/c-parser/testfiles/inner_fncalls.thy b/tools/c-parser/testfiles/inner_fncalls.thy
index 609dfc029..02a545d8e 100644
--- a/tools/c-parser/testfiles/inner_fncalls.thy
+++ b/tools/c-parser/testfiles/inner_fncalls.thy
@@ -9,7 +9,7 @@
  *)
 
 theory inner_fncalls
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "inner_fncalls.c"
diff --git a/tools/c-parser/testfiles/int_promotion.thy b/tools/c-parser/testfiles/int_promotion.thy
index 0793faa48..fbf0dfed7 100644
--- a/tools/c-parser/testfiles/int_promotion.thy
+++ b/tools/c-parser/testfiles/int_promotion.thy
@@ -9,7 +9,7 @@
  *)
 
 theory int_promotion
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "int_promotion.c"
diff --git a/tools/c-parser/testfiles/isa2014.thy b/tools/c-parser/testfiles/isa2014.thy
index 132d7368e..36f129e89 100644
--- a/tools/c-parser/testfiles/isa2014.thy
+++ b/tools/c-parser/testfiles/isa2014.thy
@@ -9,7 +9,7 @@
  *)
 
 theory isa2014
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "isa2014.c"
diff --git a/tools/c-parser/testfiles/jiraver039.thy b/tools/c-parser/testfiles/jiraver039.thy
index 0e64ba2e8..9768a9247 100644
--- a/tools/c-parser/testfiles/jiraver039.thy
+++ b/tools/c-parser/testfiles/jiraver039.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver039
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver039.c"
diff --git a/tools/c-parser/testfiles/jiraver092.thy b/tools/c-parser/testfiles/jiraver092.thy
index 9b5920c89..149f1dfc2 100644
--- a/tools/c-parser/testfiles/jiraver092.thy
+++ b/tools/c-parser/testfiles/jiraver092.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver092
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver092.c"
diff --git a/tools/c-parser/testfiles/jiraver105.thy b/tools/c-parser/testfiles/jiraver105.thy
index dff94790e..7ea0396f9 100644
--- a/tools/c-parser/testfiles/jiraver105.thy
+++ b/tools/c-parser/testfiles/jiraver105.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver105
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver105.c"
diff --git a/tools/c-parser/testfiles/jiraver110.thy b/tools/c-parser/testfiles/jiraver110.thy
index ae7f877d8..d249fa347 100644
--- a/tools/c-parser/testfiles/jiraver110.thy
+++ b/tools/c-parser/testfiles/jiraver110.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver110
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver110.c"
diff --git a/tools/c-parser/testfiles/jiraver150.thy b/tools/c-parser/testfiles/jiraver150.thy
index cdfdea6f0..1de5e814f 100644
--- a/tools/c-parser/testfiles/jiraver150.thy
+++ b/tools/c-parser/testfiles/jiraver150.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver150
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare [[use_anonymous_local_variables=true]]
diff --git a/tools/c-parser/testfiles/jiraver224.thy b/tools/c-parser/testfiles/jiraver224.thy
index d1f03c67b..884f23994 100644
--- a/tools/c-parser/testfiles/jiraver224.thy
+++ b/tools/c-parser/testfiles/jiraver224.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver224
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver224.c"
diff --git a/tools/c-parser/testfiles/jiraver253.thy b/tools/c-parser/testfiles/jiraver253.thy
index ead40cd65..d2ce2987e 100644
--- a/tools/c-parser/testfiles/jiraver253.thy
+++ b/tools/c-parser/testfiles/jiraver253.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver253
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver253.c"
diff --git a/tools/c-parser/testfiles/jiraver254.thy b/tools/c-parser/testfiles/jiraver254.thy
index 1714dcd78..15e1c0fd6 100644
--- a/tools/c-parser/testfiles/jiraver254.thy
+++ b/tools/c-parser/testfiles/jiraver254.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver254
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver254.c"
diff --git a/tools/c-parser/testfiles/jiraver307.thy b/tools/c-parser/testfiles/jiraver307.thy
index 482f90208..d9eaac0af 100644
--- a/tools/c-parser/testfiles/jiraver307.thy
+++ b/tools/c-parser/testfiles/jiraver307.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver307
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 install_C_file "jira ver307.c"
diff --git a/tools/c-parser/testfiles/jiraver310.thy b/tools/c-parser/testfiles/jiraver310.thy
index f51423415..56ceb92ed 100644
--- a/tools/c-parser/testfiles/jiraver310.thy
+++ b/tools/c-parser/testfiles/jiraver310.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver310
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver310.c"
diff --git a/tools/c-parser/testfiles/jiraver313.thy b/tools/c-parser/testfiles/jiraver313.thy
index 739177c87..613f403b7 100644
--- a/tools/c-parser/testfiles/jiraver313.thy
+++ b/tools/c-parser/testfiles/jiraver313.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver313
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 ML {* Feedback.verbosity_level := 6 *}
diff --git a/tools/c-parser/testfiles/jiraver315.thy b/tools/c-parser/testfiles/jiraver315.thy
index 13b6ef8aa..5c147792d 100644
--- a/tools/c-parser/testfiles/jiraver315.thy
+++ b/tools/c-parser/testfiles/jiraver315.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver315
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver315.c"
diff --git a/tools/c-parser/testfiles/jiraver332.thy b/tools/c-parser/testfiles/jiraver332.thy
index 93887c3b0..276a32881 100644
--- a/tools/c-parser/testfiles/jiraver332.thy
+++ b/tools/c-parser/testfiles/jiraver332.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver332
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver332.c"
diff --git a/tools/c-parser/testfiles/jiraver336.thy b/tools/c-parser/testfiles/jiraver336.thy
index a72b9cc7f..cf8d3c6bd 100644
--- a/tools/c-parser/testfiles/jiraver336.thy
+++ b/tools/c-parser/testfiles/jiraver336.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver336
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver336.c"
diff --git a/tools/c-parser/testfiles/jiraver337.thy b/tools/c-parser/testfiles/jiraver337.thy
index 4ccef66e6..ffae64ddc 100644
--- a/tools/c-parser/testfiles/jiraver337.thy
+++ b/tools/c-parser/testfiles/jiraver337.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver337
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 
diff --git a/tools/c-parser/testfiles/jiraver344.thy b/tools/c-parser/testfiles/jiraver344.thy
index 7e4faf589..5929f31ad 100644
--- a/tools/c-parser/testfiles/jiraver344.thy
+++ b/tools/c-parser/testfiles/jiraver344.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver344
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 declare [[allow_underscore_idents=true]]
diff --git a/tools/c-parser/testfiles/jiraver345.thy b/tools/c-parser/testfiles/jiraver345.thy
index 106b076d5..d57614c81 100644
--- a/tools/c-parser/testfiles/jiraver345.thy
+++ b/tools/c-parser/testfiles/jiraver345.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver345
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver345.c"
diff --git a/tools/c-parser/testfiles/jiraver384.thy b/tools/c-parser/testfiles/jiraver384.thy
index 4e7b1a094..0defa4087 100644
--- a/tools/c-parser/testfiles/jiraver384.thy
+++ b/tools/c-parser/testfiles/jiraver384.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver384
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver384.c"
diff --git a/tools/c-parser/testfiles/jiraver400.thy b/tools/c-parser/testfiles/jiraver400.thy
index 7167239aa..642a5498c 100644
--- a/tools/c-parser/testfiles/jiraver400.thy
+++ b/tools/c-parser/testfiles/jiraver400.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver400
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver400.c" [machinety=bool,roots=[h,indep1]]
diff --git a/tools/c-parser/testfiles/jiraver422.thy b/tools/c-parser/testfiles/jiraver422.thy
index 9bea1e146..0be4df326 100644
--- a/tools/c-parser/testfiles/jiraver422.thy
+++ b/tools/c-parser/testfiles/jiraver422.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver422
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver422.c"
diff --git a/tools/c-parser/testfiles/jiraver426.thy b/tools/c-parser/testfiles/jiraver426.thy
index 2833f7c15..92054b088 100644
--- a/tools/c-parser/testfiles/jiraver426.thy
+++ b/tools/c-parser/testfiles/jiraver426.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver426
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver426.c"
diff --git a/tools/c-parser/testfiles/jiraver429.thy b/tools/c-parser/testfiles/jiraver429.thy
index 5771a6381..d9cfc66a9 100644
--- a/tools/c-parser/testfiles/jiraver429.thy
+++ b/tools/c-parser/testfiles/jiraver429.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver429
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver429.c"
diff --git a/tools/c-parser/testfiles/jiraver432.thy b/tools/c-parser/testfiles/jiraver432.thy
index 052a448b6..aa993a5dd 100644
--- a/tools/c-parser/testfiles/jiraver432.thy
+++ b/tools/c-parser/testfiles/jiraver432.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver432
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver432.c"
diff --git a/tools/c-parser/testfiles/jiraver434.thy b/tools/c-parser/testfiles/jiraver434.thy
index e74755248..2cfd8eb7d 100644
--- a/tools/c-parser/testfiles/jiraver434.thy
+++ b/tools/c-parser/testfiles/jiraver434.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver434
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 
 begin
 
diff --git a/tools/c-parser/testfiles/jiraver439.thy b/tools/c-parser/testfiles/jiraver439.thy
index d40b503ec..a39a54660 100644
--- a/tools/c-parser/testfiles/jiraver439.thy
+++ b/tools/c-parser/testfiles/jiraver439.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver439
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver439.c"
diff --git a/tools/c-parser/testfiles/jiraver440.thy b/tools/c-parser/testfiles/jiraver440.thy
index 3636b667e..bb33c3ed5 100644
--- a/tools/c-parser/testfiles/jiraver440.thy
+++ b/tools/c-parser/testfiles/jiraver440.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver440
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver440.c"
diff --git a/tools/c-parser/testfiles/jiraver443.thy b/tools/c-parser/testfiles/jiraver443.thy
index ed79a8309..873c6d2d8 100644
--- a/tools/c-parser/testfiles/jiraver443.thy
+++ b/tools/c-parser/testfiles/jiraver443.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver443
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   declare [[allow_underscore_idents=true]]
diff --git a/tools/c-parser/testfiles/jiraver443a.thy b/tools/c-parser/testfiles/jiraver443a.thy
index a3dcdcd36..4d0ea5b74 100644
--- a/tools/c-parser/testfiles/jiraver443a.thy
+++ b/tools/c-parser/testfiles/jiraver443a.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver443a
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   install_C_file "jiraver443a.c"
diff --git a/tools/c-parser/testfiles/jiraver456.thy b/tools/c-parser/testfiles/jiraver456.thy
index b55e72831..0094179c1 100644
--- a/tools/c-parser/testfiles/jiraver456.thy
+++ b/tools/c-parser/testfiles/jiraver456.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver456
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 
 begin
 
diff --git a/tools/c-parser/testfiles/jiraver464.thy b/tools/c-parser/testfiles/jiraver464.thy
index 56d4e8981..0aead6fe8 100644
--- a/tools/c-parser/testfiles/jiraver464.thy
+++ b/tools/c-parser/testfiles/jiraver464.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver464
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
 (* declare [[calculate_modifies_proofs=false]] *)
diff --git a/tools/c-parser/testfiles/jiraver473.thy b/tools/c-parser/testfiles/jiraver473.thy
index ce4b93238..780db5704 100644
--- a/tools/c-parser/testfiles/jiraver473.thy
+++ b/tools/c-parser/testfiles/jiraver473.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver473
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
   declare [[munge_info_fname="jiraver473.minfo"]]
diff --git a/tools/c-parser/testfiles/jiraver54.thy b/tools/c-parser/testfiles/jiraver54.thy
index 268806706..506a28925 100644
--- a/tools/c-parser/testfiles/jiraver54.thy
+++ b/tools/c-parser/testfiles/jiraver54.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver54
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "jiraver54.c"
diff --git a/tools/c-parser/testfiles/jiraver550.thy b/tools/c-parser/testfiles/jiraver550.thy
index 02fa8f2d3..ab40e149d 100644
--- a/tools/c-parser/testfiles/jiraver550.thy
+++ b/tools/c-parser/testfiles/jiraver550.thy
@@ -11,7 +11,7 @@
 
 theory jiraver550
 imports
-  "../../../lib/CTranslationNICTA"
+  "../../../lCParser.CTranslationNICTA"
 begin
 
 install_C_file "jiraver550.c"
diff --git a/tools/c-parser/testfiles/jiraver808.thy b/tools/c-parser/testfiles/jiraver808.thy
index 2a1cfcb79..9ac7dc95b 100644
--- a/tools/c-parser/testfiles/jiraver808.thy
+++ b/tools/c-parser/testfiles/jiraver808.thy
@@ -9,7 +9,7 @@
  *)
 
 theory jiraver808
-  imports "../CTranslation"
+  imports "CParser.CTranslation"
 begin
 
  install_C_file "jiraver808.c"
diff --git a/tools/c-parser/testfiles/jiraver881.thy b/tools/c-parser/testfiles/jiraver881.thy
index 8c8c08342..348672b77 100644
--- a/tools/c-parser/testfiles/jiraver881.thy
+++ b/tools/c-parser/testfiles/jiraver881.thy
@@ -10,7 +10,7 @@
 
 theory jiraver881
 
-imports "../CTranslation"
+imports "CParser.CTranslation"
 
 begin
 
diff --git a/tools/c-parser/testfiles/kmalloc.thy b/tools/c-parser/testfiles/kmalloc.thy
index 8bf0904b3..96b12f269 100644
--- a/tools/c-parser/testfiles/kmalloc.thy
+++ b/tools/c-parser/testfiles/kmalloc.thy
@@ -9,7 +9,7 @@
  *)
 
 theory kmalloc
-imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
+imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
 begin
 
 (* no proof here, just testing the parser *)
diff --git a/tools/c-parser/testfiles/list_reverse.thy b/tools/c-parser/testfiles/list_reverse.thy
index fd511cee5..04d07f4ee 100644
--- a/tools/c-parser/testfiles/list_reverse.thy
+++ b/tools/c-parser/testfiles/list_reverse.thy
@@ -9,7 +9,7 @@
  *)
 
 theory list_reverse
-imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
+imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
 begin
 
 declare hrs_simps [simp add]
diff --git a/tools/c-parser/testfiles/list_reverse_norm.thy b/tools/c-parser/testfiles/list_reverse_norm.thy
index 14e768024..654b9e740 100644
--- a/tools/c-parser/testfiles/list_reverse_norm.thy
+++ b/tools/c-parser/testfiles/list_reverse_norm.thy
@@ -9,7 +9,7 @@
  *)
 
 theory list_reverse_norm
-imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
+imports "CParser.CTranslation" "$L4V_ARCH/imports/MachineWords"
 begin
 
 declare sep_conj_ac [simp add]
diff --git a/tools/c-parser/testfiles/locvarfncall.thy b/tools/c-parser/testfiles/locvarfncall.thy
index 67cbcf7ad..9201641b9 100644
--- a/tools/c-parser/testfiles/locvarfncall.thy
+++ b/tools/c-parser/testfiles/locvarfncall.thy
@@ -9,7 +9,7 @@
  *)
 
 theory locvarfncall
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "locvarfncall.c"
diff --git a/tools/c-parser/testfiles/longlong.thy b/tools/c-parser/testfiles/longlong.thy
index dbd61347f..11f7e0c70 100644
--- a/tools/c-parser/testfiles/longlong.thy
+++ b/tools/c-parser/testfiles/longlong.thy
@@ -9,7 +9,7 @@
  *)
 
 theory longlong
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "longlong.c"
diff --git a/tools/c-parser/testfiles/many_local_vars.thy b/tools/c-parser/testfiles/many_local_vars.thy
index e016d4fdc..1a14d9114 100644
--- a/tools/c-parser/testfiles/many_local_vars.thy
+++ b/tools/c-parser/testfiles/many_local_vars.thy
@@ -10,7 +10,7 @@
 
 theory many_local_vars
 imports
-  "../CTranslation"
+  "CParser.CTranslation"
 begin
 
 (* Avoid memory explosion caused by the C parser generating a huge record
diff --git a/tools/c-parser/testfiles/modifies_assumptions.thy b/tools/c-parser/testfiles/modifies_assumptions.thy
index a289f1cdc..344ed55e8 100644
--- a/tools/c-parser/testfiles/modifies_assumptions.thy
+++ b/tools/c-parser/testfiles/modifies_assumptions.thy
@@ -9,7 +9,7 @@
  *)
 
 theory modifies_assumptions
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "modifies_assumptions.c"
diff --git a/tools/c-parser/testfiles/modifies_speed.thy b/tools/c-parser/testfiles/modifies_speed.thy
index fd493137e..fb0211e92 100644
--- a/tools/c-parser/testfiles/modifies_speed.thy
+++ b/tools/c-parser/testfiles/modifies_speed.thy
@@ -9,7 +9,7 @@
  *)
 
 theory modifies_speed
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 text {* Speed test for modifies proofs. *}
diff --git a/tools/c-parser/testfiles/multi_deref.thy b/tools/c-parser/testfiles/multi_deref.thy
index 8073cc476..5bd63f6f9 100644
--- a/tools/c-parser/testfiles/multi_deref.thy
+++ b/tools/c-parser/testfiles/multi_deref.thy
@@ -9,7 +9,7 @@
  *)
 
 theory multi_deref
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "multi_deref.c"
diff --git a/tools/c-parser/testfiles/multidim_arrays.thy b/tools/c-parser/testfiles/multidim_arrays.thy
index 8135b79f4..9e0ed4f93 100644
--- a/tools/c-parser/testfiles/multidim_arrays.thy
+++ b/tools/c-parser/testfiles/multidim_arrays.thy
@@ -9,7 +9,7 @@
  *)
 
 theory multidim_arrays
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "multidim_arrays.c"
diff --git a/tools/c-parser/testfiles/mutrec_modifies.thy b/tools/c-parser/testfiles/mutrec_modifies.thy
index 546a6a151..6732f143d 100644
--- a/tools/c-parser/testfiles/mutrec_modifies.thy
+++ b/tools/c-parser/testfiles/mutrec_modifies.thy
@@ -9,7 +9,7 @@
  *)
 
 theory mutrec_modifies
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "mutrec_modifies.c"
diff --git a/tools/c-parser/testfiles/parse_addr.thy b/tools/c-parser/testfiles/parse_addr.thy
index e7ec30214..6d27a2931 100644
--- a/tools/c-parser/testfiles/parse_addr.thy
+++ b/tools/c-parser/testfiles/parse_addr.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_addr
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_addr.c"
diff --git a/tools/c-parser/testfiles/parse_c99block.thy b/tools/c-parser/testfiles/parse_c99block.thy
index 76a2e89a2..929ae9c92 100644
--- a/tools/c-parser/testfiles/parse_c99block.thy
+++ b/tools/c-parser/testfiles/parse_c99block.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_c99block
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_c99block.c"
diff --git a/tools/c-parser/testfiles/parse_complit.thy b/tools/c-parser/testfiles/parse_complit.thy
index e66de033b..560889ccf 100644
--- a/tools/c-parser/testfiles/parse_complit.thy
+++ b/tools/c-parser/testfiles/parse_complit.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_complit
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_complit.c"
diff --git a/tools/c-parser/testfiles/parse_dowhile.thy b/tools/c-parser/testfiles/parse_dowhile.thy
index 48fe04613..4c2026f6b 100644
--- a/tools/c-parser/testfiles/parse_dowhile.thy
+++ b/tools/c-parser/testfiles/parse_dowhile.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_dowhile
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_dowhile.c"
diff --git a/tools/c-parser/testfiles/parse_enum.thy b/tools/c-parser/testfiles/parse_enum.thy
index 64fb35988..162a91c14 100644
--- a/tools/c-parser/testfiles/parse_enum.thy
+++ b/tools/c-parser/testfiles/parse_enum.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_enum
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_enum.c"
diff --git a/tools/c-parser/testfiles/parse_fncall.thy b/tools/c-parser/testfiles/parse_fncall.thy
index f23311b54..668044911 100644
--- a/tools/c-parser/testfiles/parse_fncall.thy
+++ b/tools/c-parser/testfiles/parse_fncall.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_fncall
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_fncall.c"
diff --git a/tools/c-parser/testfiles/parse_forloop.thy b/tools/c-parser/testfiles/parse_forloop.thy
index 177841b8c..3a0953357 100644
--- a/tools/c-parser/testfiles/parse_forloop.thy
+++ b/tools/c-parser/testfiles/parse_forloop.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_forloop
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_forloop.c"
diff --git a/tools/c-parser/testfiles/parse_include.thy b/tools/c-parser/testfiles/parse_include.thy
index e0983f0c7..e184d7e08 100644
--- a/tools/c-parser/testfiles/parse_include.thy
+++ b/tools/c-parser/testfiles/parse_include.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_include
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 new_C_include_dir "includes"
diff --git a/tools/c-parser/testfiles/parse_protos.thy b/tools/c-parser/testfiles/parse_protos.thy
index 0459cb9af..a6fc6ee6b 100644
--- a/tools/c-parser/testfiles/parse_protos.thy
+++ b/tools/c-parser/testfiles/parse_protos.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_protos
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_protos.c"
diff --git a/tools/c-parser/testfiles/parse_retfncall.thy b/tools/c-parser/testfiles/parse_retfncall.thy
index 5bd9b266b..71a136610 100644
--- a/tools/c-parser/testfiles/parse_retfncall.thy
+++ b/tools/c-parser/testfiles/parse_retfncall.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_retfncall
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_retfncall.c"
diff --git a/tools/c-parser/testfiles/parse_sizeof.thy b/tools/c-parser/testfiles/parse_sizeof.thy
index 73c15ba0b..c5b9ca332 100644
--- a/tools/c-parser/testfiles/parse_sizeof.thy
+++ b/tools/c-parser/testfiles/parse_sizeof.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_sizeof
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_sizeof.c"
diff --git a/tools/c-parser/testfiles/parse_someops.thy b/tools/c-parser/testfiles/parse_someops.thy
index fbd247f6c..e4be91b3f 100644
--- a/tools/c-parser/testfiles/parse_someops.thy
+++ b/tools/c-parser/testfiles/parse_someops.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_someops
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_someops.c"
diff --git a/tools/c-parser/testfiles/parse_spec.thy.broken b/tools/c-parser/testfiles/parse_spec.thy.broken
index c16bf4279..85b752d84 100644
--- a/tools/c-parser/testfiles/parse_spec.thy.broken
+++ b/tools/c-parser/testfiles/parse_spec.thy.broken
@@ -8,7 +8,7 @@
  * @TAG(NICTA_BSD)
  *)
 
-theory parse_spec imports "../CTranslation"  begin
+theory parse_spec imports "CParser.CTranslation"  begin
 
 install_C_file "parse_spec.c"
 
diff --git a/tools/c-parser/testfiles/parse_struct.thy b/tools/c-parser/testfiles/parse_struct.thy
index 5f1cb975d..f3f3f9b74 100644
--- a/tools/c-parser/testfiles/parse_struct.thy
+++ b/tools/c-parser/testfiles/parse_struct.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_struct
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_struct.c"
diff --git a/tools/c-parser/testfiles/parse_struct_array.thy b/tools/c-parser/testfiles/parse_struct_array.thy
index c7ab4f4b2..179aa8f00 100644
--- a/tools/c-parser/testfiles/parse_struct_array.thy
+++ b/tools/c-parser/testfiles/parse_struct_array.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_struct_array
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_struct_array.c"
diff --git a/tools/c-parser/testfiles/parse_switch.thy b/tools/c-parser/testfiles/parse_switch.thy
index ab6c1d9f7..98ab80688 100644
--- a/tools/c-parser/testfiles/parse_switch.thy
+++ b/tools/c-parser/testfiles/parse_switch.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_switch
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_switch.c"
diff --git a/tools/c-parser/testfiles/parse_typecast.thy b/tools/c-parser/testfiles/parse_typecast.thy
index 7af8ebe59..36f9ac8f9 100644
--- a/tools/c-parser/testfiles/parse_typecast.thy
+++ b/tools/c-parser/testfiles/parse_typecast.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_typecast
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_typecast.c"
diff --git a/tools/c-parser/testfiles/parse_voidfn.thy b/tools/c-parser/testfiles/parse_voidfn.thy
index f430e3c8a..fdaf2e229 100644
--- a/tools/c-parser/testfiles/parse_voidfn.thy
+++ b/tools/c-parser/testfiles/parse_voidfn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory parse_voidfn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "parse_voidfn.c"
diff --git a/tools/c-parser/testfiles/phantom_mstate.thy b/tools/c-parser/testfiles/phantom_mstate.thy
index 12e428ffe..2f7ff92bf 100644
--- a/tools/c-parser/testfiles/phantom_mstate.thy
+++ b/tools/c-parser/testfiles/phantom_mstate.thy
@@ -9,7 +9,7 @@
  *)
 
 theory phantom_mstate
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "phantom_mstate.c" [machinety=bool]
diff --git a/tools/c-parser/testfiles/populate_globals.thy b/tools/c-parser/testfiles/populate_globals.thy
index 9df5407f4..e8dc830e5 100644
--- a/tools/c-parser/testfiles/populate_globals.thy
+++ b/tools/c-parser/testfiles/populate_globals.thy
@@ -9,7 +9,7 @@
  *)
 
 theory populate_globals
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare [[globals_all_addressed=true,populate_globals=true]]
diff --git a/tools/c-parser/testfiles/postfixOps.thy b/tools/c-parser/testfiles/postfixOps.thy
index f45812a6f..50640754b 100644
--- a/tools/c-parser/testfiles/postfixOps.thy
+++ b/tools/c-parser/testfiles/postfixOps.thy
@@ -9,7 +9,7 @@
  *)
 
 theory postfixOps
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "postfixOps.c"
diff --git a/tools/c-parser/testfiles/protoparamshadow.thy b/tools/c-parser/testfiles/protoparamshadow.thy
index 3eaa5e7cb..6aeddf0ae 100644
--- a/tools/c-parser/testfiles/protoparamshadow.thy
+++ b/tools/c-parser/testfiles/protoparamshadow.thy
@@ -9,7 +9,7 @@
  *)
 
 theory protoparamshadow
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "protoparamshadow.c"
diff --git a/tools/c-parser/testfiles/ptr_auxupd.thy b/tools/c-parser/testfiles/ptr_auxupd.thy
index 263143b34..cc1910c82 100644
--- a/tools/c-parser/testfiles/ptr_auxupd.thy
+++ b/tools/c-parser/testfiles/ptr_auxupd.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ptr_auxupd
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 definition
diff --git a/tools/c-parser/testfiles/ptr_diff.thy b/tools/c-parser/testfiles/ptr_diff.thy
index aca1a4be3..30103e1b6 100644
--- a/tools/c-parser/testfiles/ptr_diff.thy
+++ b/tools/c-parser/testfiles/ptr_diff.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ptr_diff
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "ptr_diff.c"
diff --git a/tools/c-parser/testfiles/ptr_modifies.thy b/tools/c-parser/testfiles/ptr_modifies.thy
index 63f081416..5160d1b91 100644
--- a/tools/c-parser/testfiles/ptr_modifies.thy
+++ b/tools/c-parser/testfiles/ptr_modifies.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ptr_modifies
-imports "../../../lib/$L4V_ARCH/WordSetup" "../CTranslation"
+imports "Word_Lib.WordSetup" "CParser.CTranslation"
 begin
 
 install_C_file "ptr_modifies.c"
diff --git a/tools/c-parser/testfiles/ptr_umm.thy.broken b/tools/c-parser/testfiles/ptr_umm.thy.broken
index e878f99b7..983bba19e 100644
--- a/tools/c-parser/testfiles/ptr_umm.thy.broken
+++ b/tools/c-parser/testfiles/ptr_umm.thy.broken
@@ -8,7 +8,7 @@
  * @TAG(NICTA_BSD)
  *)
 
-theory ptr_umm imports "../CTranslation" begin
+theory ptr_umm imports "CParser.CTranslation" begin
 
 declare sep_conj_ac [simp add]
 install_C_file "ptr_umm.c"
diff --git a/tools/c-parser/testfiles/really_simple.thy b/tools/c-parser/testfiles/really_simple.thy
index d53941b93..98131cd6c 100644
--- a/tools/c-parser/testfiles/really_simple.thy
+++ b/tools/c-parser/testfiles/really_simple.thy
@@ -9,7 +9,7 @@
  *)
 
 theory really_simple
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "really_simple.c"
diff --git a/tools/c-parser/testfiles/relspec.thy b/tools/c-parser/testfiles/relspec.thy
index 09704608f..b58cefe95 100644
--- a/tools/c-parser/testfiles/relspec.thy
+++ b/tools/c-parser/testfiles/relspec.thy
@@ -9,7 +9,7 @@
  *)
 
 theory relspec
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "relspec.c"
diff --git a/tools/c-parser/testfiles/retprefix.thy b/tools/c-parser/testfiles/retprefix.thy
index 90678de4b..45a73d9ee 100644
--- a/tools/c-parser/testfiles/retprefix.thy
+++ b/tools/c-parser/testfiles/retprefix.thy
@@ -9,7 +9,7 @@
  *)
 
 theory retprefix
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "retprefix.c"
diff --git a/tools/c-parser/testfiles/selection_sort.thy b/tools/c-parser/testfiles/selection_sort.thy
index 2204304f9..5d5e4c53d 100644
--- a/tools/c-parser/testfiles/selection_sort.thy
+++ b/tools/c-parser/testfiles/selection_sort.thy
@@ -9,7 +9,7 @@
  *)
 
 theory selection_sort
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "selection_sort.c"
diff --git a/tools/c-parser/testfiles/shortcircuit.thy b/tools/c-parser/testfiles/shortcircuit.thy
index 940ba5b03..536dc9a46 100644
--- a/tools/c-parser/testfiles/shortcircuit.thy
+++ b/tools/c-parser/testfiles/shortcircuit.thy
@@ -9,7 +9,7 @@
  *)
 
 theory shortcircuit
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "shortcircuit.c"
diff --git a/tools/c-parser/testfiles/signed_div.thy b/tools/c-parser/testfiles/signed_div.thy
index db6252f16..1067d9342 100644
--- a/tools/c-parser/testfiles/signed_div.thy
+++ b/tools/c-parser/testfiles/signed_div.thy
@@ -9,7 +9,7 @@
  *)
 
 theory signed_div
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "signed_div.c"
diff --git a/tools/c-parser/testfiles/signedoverflow.thy b/tools/c-parser/testfiles/signedoverflow.thy
index b94d047f3..8e235cae0 100644
--- a/tools/c-parser/testfiles/signedoverflow.thy
+++ b/tools/c-parser/testfiles/signedoverflow.thy
@@ -9,7 +9,7 @@
  *)
 
 theory signedoverflow
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
   install_C_file "signedoverflow.c"
diff --git a/tools/c-parser/testfiles/simple_annotated_fn.thy b/tools/c-parser/testfiles/simple_annotated_fn.thy
index 3085a5d79..dd217fbb1 100644
--- a/tools/c-parser/testfiles/simple_annotated_fn.thy
+++ b/tools/c-parser/testfiles/simple_annotated_fn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory simple_annotated_fn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 consts
diff --git a/tools/c-parser/testfiles/simple_constexpr_sizeof.thy b/tools/c-parser/testfiles/simple_constexpr_sizeof.thy
index a35f5bc3e..682a8c84f 100644
--- a/tools/c-parser/testfiles/simple_constexpr_sizeof.thy
+++ b/tools/c-parser/testfiles/simple_constexpr_sizeof.thy
@@ -9,7 +9,7 @@
  *)
 
 theory simple_constexpr_sizeof
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "simple_constexpr_sizeof.c"
diff --git a/tools/c-parser/testfiles/simple_fn.thy b/tools/c-parser/testfiles/simple_fn.thy
index d8994656c..659638bbc 100644
--- a/tools/c-parser/testfiles/simple_fn.thy
+++ b/tools/c-parser/testfiles/simple_fn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory simple_fn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "simple_fn.c"
diff --git a/tools/c-parser/testfiles/sizeof_typedef.thy b/tools/c-parser/testfiles/sizeof_typedef.thy
index 0555da4a4..54b2c3f09 100644
--- a/tools/c-parser/testfiles/sizeof_typedef.thy
+++ b/tools/c-parser/testfiles/sizeof_typedef.thy
@@ -9,7 +9,7 @@
  *)
 
 theory sizeof_typedef
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "sizeof_typedef.c"
diff --git a/tools/c-parser/testfiles/spec_annotated_fn.thy b/tools/c-parser/testfiles/spec_annotated_fn.thy
index f9adccc47..a3059856a 100644
--- a/tools/c-parser/testfiles/spec_annotated_fn.thy
+++ b/tools/c-parser/testfiles/spec_annotated_fn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory spec_annotated_fn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare sep_conj_ac [simp add]
diff --git a/tools/c-parser/testfiles/spec_annotated_voidfn.thy b/tools/c-parser/testfiles/spec_annotated_voidfn.thy
index fd34c696c..86f047c28 100644
--- a/tools/c-parser/testfiles/spec_annotated_voidfn.thy
+++ b/tools/c-parser/testfiles/spec_annotated_voidfn.thy
@@ -9,7 +9,7 @@
  *)
 
 theory spec_annotated_voidfn
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "spec_annotated_voidfn.c"
diff --git a/tools/c-parser/testfiles/swap.thy b/tools/c-parser/testfiles/swap.thy
index faf9a4587..952a0c66c 100644
--- a/tools/c-parser/testfiles/swap.thy
+++ b/tools/c-parser/testfiles/swap.thy
@@ -9,7 +9,7 @@
  *)
 
 theory swap
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare hrs_simps [simp add]
diff --git a/tools/c-parser/testfiles/switch_unsigned_signed.thy b/tools/c-parser/testfiles/switch_unsigned_signed.thy
index c4cfd47ef..037f2b7e8 100644
--- a/tools/c-parser/testfiles/switch_unsigned_signed.thy
+++ b/tools/c-parser/testfiles/switch_unsigned_signed.thy
@@ -9,7 +9,7 @@
  *)
 
 theory switch_unsigned_signed
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "switch_unsigned_signed.c"
diff --git a/tools/c-parser/testfiles/test_shifts.thy b/tools/c-parser/testfiles/test_shifts.thy
index d4a16de54..008a64e71 100644
--- a/tools/c-parser/testfiles/test_shifts.thy
+++ b/tools/c-parser/testfiles/test_shifts.thy
@@ -9,7 +9,7 @@
  *)
 
 theory test_shifts
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "test_shifts.c"
diff --git a/tools/c-parser/testfiles/ummbug20100217.thy b/tools/c-parser/testfiles/ummbug20100217.thy
index 7b20d14be..65c15f786 100644
--- a/tools/c-parser/testfiles/ummbug20100217.thy
+++ b/tools/c-parser/testfiles/ummbug20100217.thy
@@ -9,7 +9,7 @@
  *)
 
 theory ummbug20100217
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "ummbug20100217.c"
diff --git a/tools/c-parser/testfiles/untouched_globals.thy b/tools/c-parser/testfiles/untouched_globals.thy
index bd64fb9ae..3dd73fd35 100644
--- a/tools/c-parser/testfiles/untouched_globals.thy
+++ b/tools/c-parser/testfiles/untouched_globals.thy
@@ -9,7 +9,7 @@
  *)
 
 theory untouched_globals
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 declare [[record_globinits=true]]
diff --git a/tools/c-parser/testfiles/variable_munge.thy b/tools/c-parser/testfiles/variable_munge.thy
index dfd24268b..3eb32a5d7 100644
--- a/tools/c-parser/testfiles/variable_munge.thy
+++ b/tools/c-parser/testfiles/variable_munge.thy
@@ -9,7 +9,7 @@
  *)
 
 theory variable_munge
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "variable_munge.c"
diff --git a/tools/c-parser/testfiles/varinit.thy b/tools/c-parser/testfiles/varinit.thy
index 148d10eda..7103a94e4 100644
--- a/tools/c-parser/testfiles/varinit.thy
+++ b/tools/c-parser/testfiles/varinit.thy
@@ -9,7 +9,7 @@
  *)
 
 theory varinit
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "varinit.c"
diff --git a/tools/c-parser/testfiles/void_ptr_init.thy b/tools/c-parser/testfiles/void_ptr_init.thy
index 3ccba47fe..74bff884c 100644
--- a/tools/c-parser/testfiles/void_ptr_init.thy
+++ b/tools/c-parser/testfiles/void_ptr_init.thy
@@ -9,7 +9,7 @@
  *)
 
 theory void_ptr_init
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "void_ptr_init.c"
diff --git a/tools/c-parser/testfiles/volatile_asm.thy b/tools/c-parser/testfiles/volatile_asm.thy
index 7cc53c623..89536ba4f 100644
--- a/tools/c-parser/testfiles/volatile_asm.thy
+++ b/tools/c-parser/testfiles/volatile_asm.thy
@@ -9,7 +9,7 @@
  *)
 
 theory volatile_asm
-imports "../CTranslation"
+imports "CParser.CTranslation"
 begin
 
 install_C_file "volatile_asm.c"