diff --git a/proof/asmrefine/export/SEL4SimplExport.thy b/proof/asmrefine/export/SEL4SimplExport.thy index 17485d51a..c5959ce3d 100644 --- a/proof/asmrefine/export/SEL4SimplExport.thy +++ b/proof/asmrefine/export/SEL4SimplExport.thy @@ -22,7 +22,7 @@ ML \ ParseGraph.mkdir_relative @{theory} (getenv "L4V_ARCH"); val CFunDump_filename_export = getenv "L4V_ARCH" ^ "/" ^ "CFunDump.txt"; val CFunDump_filename = "export/" ^ CFunDump_filename_export; - emit_C_everything_relative @{context} (csenv ()) CFunDump_filename_export; + emit_C_everything_relative @{context} (csenv ()) CFunDump_filename_export "Kernel_C"; \ end