diff --git a/src/HOL/Library/code_test.ML b/src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML
+++ b/src/HOL/Library/code_test.ML
@@ -1,538 +1,539 @@
 (*  Title:      HOL/Library/code_test.ML
     Author:     Andreas Lochbihler, ETH Zürich
 
 Test infrastructure for the code generator.
 *)
 
 signature CODE_TEST =
 sig
   val add_driver:
     string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
     theory -> theory
   val debug: bool Config.T
   val test_terms: Proof.context -> term list -> string -> unit
   val test_code_cmd: string list -> string list -> Proof.context -> unit
   val eval_term: string -> Proof.context -> term -> term
   val check_settings: string -> string -> string -> unit
   val compile: string -> string -> unit
   val evaluate: string -> string -> string
   val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
   val ghc_options: string Config.T
   val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
   val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
   val target_Scala: string
   val target_Haskell: string
 end
 
 structure Code_Test: CODE_TEST =
 struct
 
 (* convert a list of terms into nested tuples and back *)
 
 fun mk_tuples [] = \<^Const>\<open>Unity\<close>
   | mk_tuples [t] = t
   | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
 
 fun dest_tuples \<^Const_>\<open>Pair _ _ for l r\<close> = l :: dest_tuples r
   | dest_tuples t = [t]
 
 
 fun last_field sep str =
   let
     val n = size sep
     val len = size str
     fun find i =
       if i < 0 then NONE
       else if String.substring (str, i, n) = sep then SOME i
       else find (i - 1)
   in
     (case find (len - n) of
       NONE => NONE
     | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   end
 
 fun split_first_last start stop s =
   (case first_field start s of
     NONE => NONE
   | SOME (initial, rest) =>
       (case last_field stop rest of
         NONE => NONE
       | SOME (middle, tail) => SOME (initial, middle, tail)))
 
 
 (* data slot for drivers *)
 
 structure Drivers = Theory_Data
 (
   type T =
     (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list
   val empty = []
   fun merge data : T = AList.merge (op =) (K true) data
 )
 
 val add_driver = Drivers.map o AList.update (op =)
 val get_driver = AList.lookup (op =) o Drivers.get
 
 (*
   Test drivers must produce output of the following format:
 
   The start of the relevant data is marked with start_marker,
   its end with end_marker.
 
   Between these two markers, every line corresponds to one test.
   Lines of successful tests start with success, failures start with failure.
   The failure failure may continue with the YXML encoding of the evaluated term.
   There must not be any additional whitespace in between.
 *)
 
 
 (* parsing of results *)
 
 val success = "True"
 val failure = "False"
 val start_marker = "*@*Isabelle/Code_Test-start*@*"
 val end_marker = "*@*Isabelle/Code_Test-end*@*"
 
 fun parse_line line =
   if String.isPrefix success line then (true, NONE)
   else if String.isPrefix failure line then (false,
     if size line > size failure then
       String.extract (line, size failure, NONE)
       |> YXML.parse_body
       |> Term_XML.Decode.term_raw
       |> dest_tuples
       |> SOME
     else NONE)
   else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
 
 fun parse_result target out =
   (case split_first_last start_marker end_marker out of
     NONE => error ("Evaluation failed for " ^ target ^ "!\nCompiler output:\n" ^ out)
   | SOME (_, middle, _) => middle |> trim_split_lines |> map parse_line)
 
 
 (* pretty printing of test results *)
 
 fun pretty_eval _ NONE _ = []
   | pretty_eval ctxt (SOME evals) ts =
       [Pretty.fbrk,
        Pretty.big_list "Evaluated terms"
          (map (fn (t, eval) => Pretty.block
            [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
             Syntax.pretty_term ctxt eval])
          (ts ~~ evals))]
 
 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @
     [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @
     pretty_eval ctxt evals eval_ts)
 
 fun pretty_failures ctxt target failures =
   Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
 
 
 (* driver invocation *)
 
 val debug = Attrib.setup_config_bool \<^binding>\<open>test_code_debug\<close> (K false)
 
 fun with_debug_dir name f =
   (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
   |> Exn.capture f
   |> Exn.release;
 
 fun dynamic_value_strict ctxt t compiler =
   let
     val thy = Proof_Context.theory_of ctxt
     val (driver, target) =
       (case get_driver thy compiler of
         NONE => error ("No driver for target " ^ compiler)
       | SOME drv => drv)
     val with_dir = if Config.get ctxt debug then with_debug_dir else Isabelle_System.with_tmp_dir
     fun eval result =
-      with_dir "Code_Test" (driver ctxt ((apfst o map o apfst) Long_Name.implode result))
+      with_dir "Code_Test"
+        (driver ctxt ((apfst o map) (apfst Long_Name.implode #> apsnd Bytes.content) result))
       |> parse_result compiler
     fun evaluator program _ vs_ty deps =
       Exn.interruptible_capture eval
         (Code_Target.compilation_text ctxt target program deps true vs_ty)
     fun postproc f = map (apsnd (Option.map (map f)))
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 
 (* term preprocessing *)
 
 fun add_eval \<^Const_>\<open>Trueprop for t\<close> = add_eval t
   | add_eval \<^Const_>\<open>HOL.eq _ for lhs rhs\<close> = (fn acc =>
       acc
       |> add_eval rhs
       |> add_eval lhs
       |> cons rhs
       |> cons lhs)
   | add_eval \<^Const_>\<open>Not for t\<close> = add_eval t
   | add_eval \<^Const_>\<open>less_eq _ for lhs rhs\<close> = (fn acc => lhs :: rhs :: acc)
   | add_eval \<^Const_>\<open>less _ for lhs rhs\<close> = (fn acc => lhs :: rhs :: acc)
   | add_eval _ = I
 
 fun mk_term_of [] = \<^Const>\<open>None \<^typ>\<open>unit \<Rightarrow> yxml_of_term\<close>\<close>
   | mk_term_of ts =
       let
         val tuple = mk_tuples ts
         val T = fastype_of tuple
       in
         \<^Const>\<open>Some \<^typ>\<open>unit \<Rightarrow> yxml_of_term\<close> for
           \<open>absdummy \<^Type>\<open>unit\<close>
             \<^Const>\<open>yxml_string_of_term for \<^Const>\<open>Code_Evaluation.term_of T for tuple\<close>\<close>\<close>\<close>
       end
 
 fun test_terms ctxt ts target =
   let
     val thy = Proof_Context.theory_of ctxt
 
     fun term_of t = Sign.of_sort thy (fastype_of t, \<^sort>\<open>term_of\<close>)
 
     fun ensure_bool t =
       (case fastype_of t of
         \<^Type>\<open>bool\<close> => ()
       | _ =>
         error (Pretty.string_of
           (Pretty.block [Pretty.str "Test case not of type bool:", Pretty.brk 1,
             Syntax.pretty_term ctxt t])))
 
     val _ = List.app ensure_bool ts
 
     val evals = map (fn t => filter term_of (add_eval t [])) ts
     val eval = map mk_term_of evals
 
     val t =
       HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close>
         (map HOLogic.mk_prod (ts ~~ eval))
 
     val result = dynamic_value_strict ctxt t target
 
     val failed =
       filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
       handle ListPair.UnequalLengths =>
         error ("Evaluation failed!\nWrong number of test results: " ^ string_of_int (length result))
   in
     (case failed of
       [] => ()
     | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
   end
 
 fun test_code_cmd raw_ts targets ctxt =
   let
     val ts = Syntax.read_terms ctxt raw_ts
     val frees = fold Term.add_frees ts []
     val _ =
       if null frees then ()
       else error (Pretty.string_of
         (Pretty.block (Pretty.str "Terms contain free variables:" :: Pretty.brk 1 ::
           Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
   in List.app (test_terms ctxt ts) targets end
 
 fun eval_term target ctxt t =
   let
     val frees = Term.add_frees t []
     val _ =
       if null frees then ()
       else
         error (Pretty.string_of
           (Pretty.block (Pretty.str "Term contains free variables:" :: Pretty.brk 1 ::
             Pretty.commas (map (Syntax.pretty_term ctxt o Free) frees))))
 
     val T = fastype_of t
     val _ =
       if Sign.of_sort (Proof_Context.theory_of ctxt) (T, \<^sort>\<open>term_of\<close>) then ()
       else error ("Type " ^ Syntax.string_of_typ ctxt T ^
        " of term not of sort " ^ Syntax.string_of_sort ctxt \<^sort>\<open>term_of\<close>)
 
     val t' =
       HOLogic.mk_list \<^typ>\<open>bool \<times> (unit \<Rightarrow> yxml_of_term) option\<close>
         [HOLogic.mk_prod (\<^Const>\<open>False\<close>, mk_term_of [t])]
 
     val result = dynamic_value_strict ctxt t' target
   in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
 
 
 (* check and invoke compiler *)
 
 fun check_settings compiler var descr =
   if getenv var = "" then
     error (Pretty.string_of (Pretty.para
       ("Environment variable " ^ var ^ " is not set. To test code generation with " ^
         compiler ^ ", set this variable to your " ^ descr ^
         " in the $ISABELLE_HOME_USER/etc/settings file.")))
   else ()
 
 fun compile compiler cmd =
   let val (out, ret) = Isabelle_System.bash_output cmd in
     if ret = 0 then ()
     else error ("Compilation with " ^ compiler ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   end
 
 fun evaluate compiler cmd =
   let val (out, res) = Isabelle_System.bash_output cmd in
     if res = 0 then out
     else error ("Evaluation for " ^ compiler ^ " terminated with error code " ^
       string_of_int res ^ "\nCompiler output:\n" ^ out)
   end
 
 
 (* driver for PolyML *)
 
 val polymlN = "PolyML"
 
 fun evaluate_in_polyml (_: Proof.context) (code_files, value_name) dir =
   let
     val code_path = dir + Path.basic "generated.sml"
     val driver_path = dir + Path.basic "driver.sml"
     val out_path = dir + Path.basic "out"
 
     val code = #2 (the_single code_files)
     val driver = \<^verbatim>\<open>
 fun main () =
   let
     fun format (true, _) = \<close> ^ ML_Syntax.print_string success ^ \<^verbatim>\<open> ^ "\n"
       | format (false, NONE) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ "\n"
       | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ t () ^ "\n"
     val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
     val result_text = \<close> ^
       ML_Syntax.print_string start_marker ^
       \<^verbatim>\<open> ^ String.concat (map format result) ^ \<close> ^
       ML_Syntax.print_string end_marker ^ \<^verbatim>\<open>
     val out = BinIO.openOut \<close> ^ ML_Syntax.print_platform_path out_path ^ \<^verbatim>\<open>
     val _ = BinIO.output (out, Byte.stringToBytes result_text)
     val _ = BinIO.closeOut out
   in () end;
 \<close>
     val _ = File.write code_path code
     val _ = File.write driver_path driver
     val _ =
       ML_Context.eval
         {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
           writeln = writeln, warning = warning}
         Position.none
         (ML_Lex.read_text (code, Path.position code_path) @
          ML_Lex.read_text (driver, Path.position driver_path) @
          ML_Lex.read "main ()")
       handle ERROR msg => error ("Evaluation for " ^ polymlN ^ " failed:\n" ^ msg)
   in File.read out_path end
 
 
 (* driver for mlton *)
 
 val mltonN = "MLton"
 val ISABELLE_MLTON = "ISABELLE_MLTON"
 
 fun evaluate_in_mlton (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = mltonN
     val generatedN = "generated.sml"
     val driverN = "driver.sml"
     val projectN = "test"
 
     val code_path = dir + Path.basic generatedN
     val driver_path = dir + Path.basic driverN
     val basis_path = dir + Path.basic (projectN ^ ".mlb")
     val driver = \<^verbatim>\<open>
 fun format (true, _) = \<close> ^ ML_Syntax.print_string success ^ \<^verbatim>\<open> ^ "\n"
   | format (false, NONE) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ "\n"
   | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ t () ^ "\n"
 val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
 val _ = print \<close> ^ ML_Syntax.print_string start_marker ^ \<^verbatim>\<open>
 val _ = List.app (print o format) result
 val _ = print \<close> ^ ML_Syntax.print_string end_marker ^ \<^verbatim>\<open>
 \<close>
     val _ = check_settings compiler ISABELLE_MLTON "MLton executable"
     val _ = List.app (File.write code_path o snd) code_files
     val _ = File.write driver_path driver
     val _ = File.write basis_path ("$(SML_LIB)/basis/basis.mlb\n" ^ generatedN ^ "\n" ^ driverN)
   in
     compile compiler ("\"$ISABELLE_MLTON\" -default-type intinf " ^ File.bash_path basis_path);
     evaluate compiler (File.bash_path (dir + Path.basic projectN))
   end
 
 
 (* driver for SML/NJ *)
 
 val smlnjN = "SMLNJ"
 val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
 
 fun evaluate_in_smlnj (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = smlnjN
     val generatedN = "generated.sml"
     val driverN = "driver.sml"
 
     val code_path = dir + Path.basic generatedN
     val driver_path = dir + Path.basic driverN
     val driver = \<^verbatim>\<open>
 structure Test =
 struct
   fun main () =
     let
       fun format (true, _) = \<close> ^ ML_Syntax.print_string success ^ \<^verbatim>\<open> ^ "\n"
         | format (false, NONE) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ "\n"
         | format (false, SOME t) = \<close> ^ ML_Syntax.print_string failure ^ \<^verbatim>\<open> ^ t () ^ "\n"
       val result = \<close> ^ value_name ^ \<^verbatim>\<open> ()
       val _ = print \<close> ^ ML_Syntax.print_string start_marker ^ \<^verbatim>\<open>
       val _ = List.app (print o format) result
       val _ = print \<close> ^ ML_Syntax.print_string end_marker ^ \<^verbatim>\<open>
     in 0 end
 end
 \<close>
     val _ = check_settings compiler ISABELLE_SMLNJ "SMLNJ executable"
     val _ = List.app (File.write code_path o snd) code_files
     val _ = File.write driver_path driver
     val ml_source =
       "Control.MC.matchRedundantError := false; Control.MC.matchRedundantWarn := false;" ^
       "use " ^ ML_Syntax.print_string (File.platform_path code_path) ^
       "; use " ^ ML_Syntax.print_string (File.platform_path driver_path) ^
       "; Test.main ();"
   in evaluate compiler ("echo " ^ Bash.string ml_source ^ " | \"$ISABELLE_SMLNJ\"") end
 
 
 (* driver for OCaml *)
 
 val ocamlN = "OCaml"
 val ISABELLE_OCAMLFIND = "ISABELLE_OCAMLFIND"
 
 fun evaluate_in_ocaml (_: Proof.context) (code_files, value_name) dir =
   let
     val compiler = ocamlN
 
     val code_path = dir + Path.basic "generated.ml"
     val driver_path = dir + Path.basic "driver.ml"
     val driver =
       "let format_term = function\n" ^
       "  | None -> \"\"\n" ^
       "  | Some t -> t ();;\n" ^
       "let format = function\n" ^
       "  | (true, _) -> \"" ^ success ^ "\\n\"\n" ^
       "  | (false, x) -> \"" ^ failure ^ "\" ^ format_term x ^ \"\\n\";;\n" ^
       "let result = " ^ ("Generated." ^ value_name) ^ " ();;\n" ^
       "let main x =\n" ^
       "  let _ = print_string \"" ^ start_marker ^ "\" in\n" ^
       "  let _ = List.map (fun x -> print_string (format x)) result in\n" ^
       "  print_string \"" ^ end_marker ^ "\";;\n" ^
       "main ();;"
     val compiled_path = dir + Path.basic "test"
 
     val _ = check_settings compiler ISABELLE_OCAMLFIND "ocamlfind executable"
     val _ = List.app (File.write code_path o snd) code_files
     val _ = File.write driver_path driver
     val cmd =
       "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path dir ^ " " ^
       File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
   in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end
 
 
 (* driver for GHC *)
 
 val ghcN = "GHC"
 val ISABELLE_GHC = "ISABELLE_GHC"
 
 val ghc_options = Attrib.setup_config_string \<^binding>\<open>code_test_ghc\<close> (K "")
 
 fun evaluate_in_ghc ctxt (code_files, value_name) dir =
   let
     val compiler = ghcN
     val modules = map fst code_files
 
     val driver_path = dir + Path.basic "Main.hs"
     val driver =
       "module Main where {\n" ^
       implode (map (fn module => "import qualified " ^ unsuffix ".hs" module ^ ";\n") modules) ^
       "main = do {\n" ^
       "    let {\n" ^
       "      format_term Nothing = \"\";\n" ^
       "      format_term (Just t) = t ();\n" ^
       "      format (True, _) = \"" ^ success ^ "\\n\";\n" ^
       "      format (False, to) = \"" ^ failure ^ "\" ++ format_term to ++ \"\\n\";\n" ^
       "      result = " ^ value_name ^ " ();\n" ^
       "    };\n" ^
       "    Prelude.putStr \"" ^ start_marker ^ "\";\n" ^
       "    Prelude.mapM_ (putStr . format) result;\n" ^
       "    Prelude.putStr \"" ^ end_marker ^ "\";\n" ^
       "  }\n" ^
       "}\n"
 
     val _ = check_settings compiler ISABELLE_GHC "GHC executable"
     val _ = List.app (fn (name, code) => File.write (dir + Path.basic name) code) code_files
     val _ = File.write driver_path driver
 
     val compiled_path = dir + Path.basic "test"
     val cmd =
       "\"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
       Config.get ctxt ghc_options ^ " -o " ^
       File.bash_platform_path compiled_path ^ " " ^
       File.bash_platform_path driver_path ^ " -i" ^
       File.bash_platform_path dir
   in compile compiler cmd; evaluate compiler (File.bash_path compiled_path) end
 
 
 (* driver for Scala *)
 
 val scalaN = "Scala"
 
 fun evaluate_in_scala (_: Proof.context) (code_files, value_name) dir =
   let
     val generatedN = "Generated_Code"
     val driverN = "Driver.scala"
 
     val code_path = dir + Path.basic (generatedN ^ ".scala")
     val driver_path = dir + Path.basic driverN
     val out_path = dir + Path.basic "out"
 
     val code = #2 (the_single code_files)
     val driver = \<^verbatim>\<open>
 {
   val result = \<close> ^ value_name ^ \<^verbatim>\<open>(())
   val result_text =
     result.map(
       {
         case (true, _) => "True\n"
         case (false, None) => "False\n"
         case (false, Some(t)) => "False" + t(()) + "\n"
       }).mkString
   isabelle.File.write(
     isabelle.Path.explode(\<close> ^ quote (Path.implode (Path.expand out_path)) ^ \<^verbatim>\<open>),
     \<close> ^ quote start_marker ^ \<^verbatim>\<open> + result_text + \<close> ^ quote end_marker ^ \<^verbatim>\<open>)
 }\<close>
     val _ = File.write code_path code
     val _ = File.write driver_path driver
     val _ = Scala_Compiler.toplevel true (code ^ driver)
       handle ERROR msg => error ("Evaluation for " ^ scalaN ^ " failed:\n" ^ msg)
   in File.read out_path end
 
 
 (* command setup *)
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>test_code\<close>
     "compile test cases to target languages, execute them and report results"
       (Scan.repeat1 Parse.prop -- (\<^keyword>\<open>in\<close> |-- Scan.repeat1 Parse.name)
         >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
 
 val target_Scala = "Scala_eval"
 val target_Haskell = "Haskell_eval"
 
 val _ =
   Theory.setup
    (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) #>
     Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)]) #>
     fold add_driver
       [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
        (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
        (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
        (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
        (ghcN, (evaluate_in_ghc, target_Haskell)),
        (scalaN, (evaluate_in_scala, target_Scala))] #>
     fold (fn target => Value_Command.add_evaluator (Binding.name target, eval_term target) #> #2)
       [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
 
 end
diff --git a/src/HOL/Tools/Quickcheck/narrowing_generators.ML b/src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML
@@ -1,549 +1,550 @@
 (*  Title:      HOL/Tools/Quickcheck/narrowing_generators.ML
     Author:     Lukas Bulwahn, TU Muenchen
 
 Narrowing-based counterexample generation.
 *)
 
 signature NARROWING_GENERATORS =
 sig
   val allow_existentials : bool Config.T
   val finite_functions : bool Config.T
   val overlord : bool Config.T
   val ghc_options : string Config.T  (* FIXME prefer settings, i.e. getenv (!?) *)
   val active : bool Config.T
   datatype counterexample = Universal_Counterexample of (term * counterexample)
     | Existential_Counterexample of (term * counterexample) list
     | Empty_Assignment
   val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
   val put_existential_counterexample : (unit -> counterexample option) ->
     Proof.context -> Proof.context
 end
 
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
 (* configurations *)
 
 val allow_existentials = Attrib.setup_config_bool \<^binding>\<open>quickcheck_allow_existentials\<close> (K true)
 val finite_functions = Attrib.setup_config_bool \<^binding>\<open>quickcheck_finite_functions\<close> (K true)
 val overlord = Attrib.setup_config_bool \<^binding>\<open>quickcheck_narrowing_overlord\<close> (K false)
 val ghc_options = Attrib.setup_config_string \<^binding>\<open>quickcheck_narrowing_ghc_options\<close> (K "")
 
 
 (* partial_term_of instances *)
 
 fun mk_partial_term_of (x, T) =
   Const (\<^const_name>\<open>Quickcheck_Narrowing.partial_term_of_class.partial_term_of\<close>,
     Term.itselfT T --> \<^typ>\<open>narrowing_term\<close> --> \<^typ>\<open>Code_Evaluation.term\<close>) $ Logic.mk_type T $ x
 
 
 (** formal definition **)
 
 fun add_partial_term_of tyco raw_vs thy =
   let
     val vs = map (fn (v, _) => (v, \<^sort>\<open>typerep\<close>)) raw_vs
     val ty = Type (tyco, map TFree vs)
     val lhs =
       Const (\<^const_name>\<open>partial_term_of\<close>,
         Term.itselfT ty --> \<^typ>\<open>narrowing_term\<close> --> \<^typ>\<open>Code_Evaluation.term\<close>) $
       Free ("x", Term.itselfT ty) $ Free ("t", \<^typ>\<open>narrowing_term\<close>)
     val rhs = \<^term>\<open>undefined :: Code_Evaluation.term\<close>
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
     fun triv_name_of t =
       (fst o dest_Free o fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^
         "_triv"
   in
     thy
     |> Class.instantiation ([tyco], vs, \<^sort>\<open>partial_term_of\<close>)
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end
 
 fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
   let
     val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\<open>partial_term_of\<close>)
       andalso Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\<open>typerep\<close>
   in if need_inst then add_partial_term_of tyco raw_vs thy else thy end
 
 
 (** code equations for datatypes **)
 
 fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
   let
     val frees = map Free (Name.invent_names Name.context "a" (map (K \<^typ>\<open>narrowing_term\<close>) tys))
     val narrowing_term =
       \<^term>\<open>Quickcheck_Narrowing.Narrowing_constructor\<close> $ HOLogic.mk_number \<^typ>\<open>integer\<close> i $
         HOLogic.mk_list \<^typ>\<open>narrowing_term\<close> (rev frees)
     val rhs =
       fold (fn u => fn t => \<^term>\<open>Code_Evaluation.App\<close> $ t $ u)
         (map mk_partial_term_of (frees ~~ tys))
         (\<^term>\<open>Code_Evaluation.Const\<close> $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
     val insts =
       map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
         [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
     val cty = Thm.global_ctyp_of thy ty
   in
     @{thm partial_term_of_anything}
     |> Thm.instantiate' [SOME cty] insts
     |> Thm.varifyT_global
   end
 
 fun add_partial_term_of_code tyco raw_vs raw_cs thy =
   let
     val algebra = Sign.classes_of thy
     val vs = map (fn (v, sort) => (v, curry (Sorts.inter_sort algebra) \<^sort>\<open>typerep\<close> sort)) raw_vs
     val ty = Type (tyco, map TFree vs)
     val cs =
       (map o apsnd o apsnd o map o map_atyps)
         (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs
     val const = Axclass.param_of_inst thy (\<^const_name>\<open>partial_term_of\<close>, tyco)
     val var_insts =
       map (SOME o Thm.global_cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
         [Free ("ty", Term.itselfT ty), \<^term>\<open>Quickcheck_Narrowing.Narrowing_variable p tt\<close>,
           \<^term>\<open>Code_Evaluation.Free (STR ''_'')\<close> $ HOLogic.mk_typerep ty]
     val var_eq =
       @{thm partial_term_of_anything}
       |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts
       |> Thm.varifyT_global
     val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
   in
     thy
     |> Code.declare_default_eqns_global (map (rpair true) eqs)
   end
 
 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
   let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco \<^sort>\<open>partial_term_of\<close>
   in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end
 
 
 (* narrowing generators *)
 
 (** narrowing specific names and types **)
 
 exception FUNCTION_TYPE
 
 val narrowingN = "narrowing"
 
 fun narrowingT T = \<^typ>\<open>integer\<close> --> Type (\<^type_name>\<open>Quickcheck_Narrowing.narrowing_cons\<close>, [T])
 
 fun mk_cons c T = Const (\<^const_name>\<open>Quickcheck_Narrowing.cons\<close>, T --> narrowingT T) $ Const (c, T)
 
 fun mk_apply (T, t) (U, u) =
   let
     val (_, U') = dest_funT U
   in
     (U', Const (\<^const_name>\<open>Quickcheck_Narrowing.apply\<close>,
       narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
   end
 
 fun mk_sum (t, u) =
   let val T = fastype_of t
   in Const (\<^const_name>\<open>Quickcheck_Narrowing.sum\<close>, T --> T --> T) $ t $ u end
 
 
 (** deriving narrowing instances **)
 
 fun mk_equations descr vs narrowings =
   let
     fun mk_call T =
       (T, Const (\<^const_name>\<open>Quickcheck_Narrowing.narrowing_class.narrowing\<close>, narrowingT T))
     fun mk_aux_call fTs (k, _) (tyco, Ts) =
       let
         val T = Type (tyco, Ts)
         val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
       in
         (T, nth narrowings k)
       end
     fun mk_consexpr simpleT (c, xs) =
       let val Ts = map fst xs
       in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
     fun mk_rhs exprs = foldr1 mk_sum exprs
     val rhss =
       Old_Datatype_Aux.interpret_construction descr vs
         { atyp = mk_call, dtyp = mk_aux_call }
       |> (map o apfst) Type
       |> map (fn (T, cs) => map (mk_consexpr T) cs)
       |> map mk_rhs
     val lhss = narrowings
     val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
   in eqs end
 
 fun contains_recursive_type_under_function_types xs =
   exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
     (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
 
 fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = Old_Datatype_Aux.message config "Creating narrowing generators ..."
     val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames)
   in
     if not (contains_recursive_type_under_function_types descr) then
       thy
       |> Class.instantiation (tycos, vs, \<^sort>\<open>narrowing\<close>)
       |> Quickcheck_Common.define_functions
         (fn narrowings => mk_equations descr vs narrowings, NONE)
         prfx [] narrowingsN (map narrowingT (Ts @ Us))
       |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
     else thy
   end
 
 
 (* testing framework *)
 
 val target = "Haskell_Quickcheck"
 
 
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine =
   File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
 
 val pnf_narrowing_engine =
   File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
 
 fun exec verbose code =
   ML_Context.exec (fn () =>
     ML_Compiler0.ML ML_Env.context
       {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
   (Path.explode "$ISABELLE_HOME_USER" + Path.basic (name ^ serial_string ()))
   |> Isabelle_System.make_directory
   |> Exn.capture f
   |> Exn.release
 
 fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size))
-    ctxt cookie (code_modules, _) =
+    ctxt cookie (code_modules_bytes, _) =
   let
+    val code_modules = (map o apsnd) Bytes.content code_modules_bytes
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else writeln s
     fun verbose_message s = if not quiet andalso verbose then writeln s else ()
     val current_size = Unsynchronized.ref 0
     val current_result = Unsynchronized.ref Quickcheck.empty_result
     val tmp_prefix = "Quickcheck_Narrowing"
     val ghc_options = Config.get ctxt ghc_options
     val with_tmp_dir =
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
     fun run in_path =
       let
         fun mk_code_file module =
           let
             val (paths, base) = split_last module
           in Path.appends (in_path :: map Path.basic (paths @ [suffix ".hs" base])) end;
         val generatedN_suffix = suffix ".hs" Code_Target.generatedN;
         val includes = AList.delete (op =) [generatedN_suffix] code_modules
           |> (map o apfst) mk_code_file
         val code = the (AList.lookup (op =) code_modules [generatedN_suffix])
         val code_file = mk_code_file [Code_Target.generatedN]
         val narrowing_engine_file = mk_code_file ["Narrowing_Engine"]
         val main_file = mk_code_file ["Main"]
         val main =
           "module Main where {\n\n" ^
           "import System.IO;\n" ^
           "import System.Environment;\n" ^
           "import Narrowing_Engine;\n" ^
           "import " ^ Code_Target.generatedN ^ " ;\n\n" ^
           "main = getArgs >>= \\[potential, size] -> " ^
           "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ Code_Target.generatedN ^
           ".value ())\n\n}\n"
         val _ =
           map (uncurry File.write)
             (includes @
               [(narrowing_engine_file,
                 if contains_existentials then pnf_narrowing_engine else narrowing_engine),
                (code_file, code), (main_file, main)])
         val executable = in_path + Path.basic "isabelle_quickcheck_narrowing"
         val cmd =
           "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^ ghc_options ^ " " ^
             (space_implode " "
               (map File.bash_platform_path
                 (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
           " -o " ^ File.bash_platform_path executable ^ ";"
         val compilation_time =
           Isabelle_System.bash_process (Bash.script cmd)
           |> Process_Result.check
           |> Process_Result.timing_elapsed |> Time.toMilliseconds
           handle ERROR msg => cat_error "Compilation with GHC failed" msg
         val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
         fun with_size genuine_only k =
           if k > size then (NONE, !current_result)
           else
             let
               val _ = verbose_message ("[Quickcheck-narrowing] Test data size: " ^ string_of_int k)
               val _ = current_size := k
               val res =
                 Isabelle_System.bash_process (Bash.script
                   (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
                     string_of_int k))
                 |> Process_Result.check
               val response = Process_Result.out res
               val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds;
               val _ =
                 Quickcheck.add_timing
                   ("execution of size " ^ string_of_int k, timing) current_result
             in
               if response = "NONE" then with_size genuine_only (k + 1)
               else
                 let
                   val output_value = the_default "NONE"
                     (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
                   val ml_code =
                     "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml
                     ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))"
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
                     |> Context.proof_map (exec false ml_code)
                   val counterexample = get ctxt' ()
                 in
                   if is_genuine counterexample then
                     (counterexample, !current_result)
                   else
                     let
                       val cex = Option.map (rpair []) (counterexample_of counterexample)
                       val _ = message (Pretty.string_of (Quickcheck.pretty_counterex ctxt false cex))
                       val _ = message "Quickcheck continues to find a genuine counterexample..."
                     in with_size true (k + 1) end
                end
             end
       in with_size genuine_only 0 end
   in with_tmp_dir tmp_prefix run end
 
 fun dynamic_value_strict opts cookie ctxt postproc t =
   let
     fun evaluator program _ vs_ty_t deps =
       Exn.interruptible_capture (value opts ctxt cookie)
         (Code_Target.compilation_text ctxt target program deps true vs_ty_t)
   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
 
 
 (** counterexample generator **)
 
 datatype counterexample =
     Universal_Counterexample of (term * counterexample)
   | Existential_Counterexample of (term * counterexample) list
   | Empty_Assignment
 
 fun map_counterexample _ Empty_Assignment = Empty_Assignment
   | map_counterexample f (Universal_Counterexample (t, c)) =
       Universal_Counterexample (f t, map_counterexample f c)
   | map_counterexample f (Existential_Counterexample cs) =
       Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
 
 structure Data = Proof_Data
 (
   type T =
     (unit -> (bool * term list) option) *
     (unit -> counterexample option)
   val empty: T =
    (fn () => raise Fail "counterexample",
     fn () => raise Fail "existential_counterexample")
   fun init _ = empty
 )
 
 val get_counterexample = #1 o Data.get;
 val get_existential_counterexample = #2 o Data.get;
 
 val put_counterexample = Data.map o @{apply 2(1)} o K
 val put_existential_counterexample = Data.map o @{apply 2(2)} o K
 
 fun finitize_functions (xTs, t) =
   let
     val (names, boundTs) = split_list xTs
     fun mk_eval_ffun dT rT =
       Const (\<^const_name>\<open>Quickcheck_Narrowing.eval_ffun\<close>,
         Type (\<^type_name>\<open>Quickcheck_Narrowing.ffun\<close>, [dT, rT]) --> dT --> rT)
     fun mk_eval_cfun dT rT =
       Const (\<^const_name>\<open>Quickcheck_Narrowing.eval_cfun\<close>,
         Type (\<^type_name>\<open>Quickcheck_Narrowing.cfun\<close>, [rT]) --> dT --> rT)
     fun eval_function (Type (\<^type_name>\<open>fun\<close>, [dT, rT])) =
           let
             val (rt', rT') = eval_function rT
           in
             (case dT of
               Type (\<^type_name>\<open>fun\<close>, _) =>
                 (fn t => absdummy dT (rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
                   Type (\<^type_name>\<open>Quickcheck_Narrowing.cfun\<close>, [rT']))
             | _ =>
                 (fn t => absdummy dT (rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
                   Type (\<^type_name>\<open>Quickcheck_Narrowing.ffun\<close>, [dT, rT'])))
           end
       | eval_function (T as Type (\<^type_name>\<open>prod\<close>, [fT, sT])) =
           let
             val (ft', fT') = eval_function fT
             val (st', sT') = eval_function sT
             val T' = Type (\<^type_name>\<open>prod\<close>, [fT', sT'])
             val map_const = Const (\<^const_name>\<open>map_prod\<close>, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
             fun apply_dummy T t = absdummy T (t (Bound 0))
           in
             (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
           end
       | eval_function T = (I, T)
     val (tt, boundTs') = split_list (map eval_function boundTs)
     val t' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) boundTs), t)
   in
     (names ~~ boundTs', t')
   end
 
 fun dest_ffun (Type (\<^type_name>\<open>Quickcheck_Narrowing.ffun\<close>, [dT, rT])) = (dT, rT)
 
 fun eval_finite_functions (Const (\<^const_name>\<open>Quickcheck_Narrowing.ffun.Constant\<close>, T) $ value) =
       absdummy (fst (dest_ffun (body_type T))) (eval_finite_functions value)
   | eval_finite_functions (Const (\<^const_name>\<open>Quickcheck_Narrowing.ffun.Update\<close>, T) $ a $ b $ f) =
       let
         val (T1, T2) = dest_ffun (body_type T)
       in
         Quickcheck_Common.mk_fun_upd T1 T2
           (eval_finite_functions a, eval_finite_functions b) (eval_finite_functions f)
       end
   | eval_finite_functions t = t
 
 
 (** tester **)
 
 val rewrs =
   map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
     (@{thms all_simps} @ @{thms ex_simps}) @
   map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of)
     [@{thm iff_conv_conj_imp}, @{thm not_ex}, @{thm not_all},
      @{thm meta_eq_to_obj_eq [OF Ex1_def]}]
 
 fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
 
 fun strip_quantifiers (Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (x, T, t)) =
       apfst (cons (\<^const_name>\<open>Ex\<close>, (x, T))) (strip_quantifiers t)
   | strip_quantifiers (Const (\<^const_name>\<open>All\<close>, _) $ Abs (x, T, t)) =
       apfst (cons (\<^const_name>\<open>All\<close>, (x, T))) (strip_quantifiers t)
   | strip_quantifiers t = ([], t)
 
 fun contains_existentials t =
   exists (fn (Q, _) => Q = \<^const_name>\<open>Ex\<close>) (fst (strip_quantifiers t))
 
 fun mk_property qs t =
   let
     fun enclose (\<^const_name>\<open>Ex\<close>, (x, T)) t =
           Const (\<^const_name>\<open>Quickcheck_Narrowing.exists\<close>,
             (T --> \<^typ>\<open>property\<close>) --> \<^typ>\<open>property\<close>) $ Abs (x, T, t)
       | enclose (\<^const_name>\<open>All\<close>, (x, T)) t =
           Const (\<^const_name>\<open>Quickcheck_Narrowing.all\<close>,
             (T --> \<^typ>\<open>property\<close>) --> \<^typ>\<open>property\<close>) $ Abs (x, T, t)
   in fold_rev enclose qs (\<^term>\<open>Quickcheck_Narrowing.Property\<close> $ t) end
 
 fun mk_case_term ctxt p ((\<^const_name>\<open>Ex\<close>, (x, T)) :: qs') (Existential_Counterexample cs) =
       Case_Translation.make_case ctxt Case_Translation.Quiet Name.context (Free (x, T)) (map (fn (t, c) =>
         (t, mk_case_term ctxt (p - 1) qs' c)) cs)
   | mk_case_term ctxt p ((\<^const_name>\<open>All\<close>, _) :: qs') (Universal_Counterexample (t, c)) =
       if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
 
 val post_process =
   perhaps (try Quickcheck_Common.post_process_term) o eval_finite_functions
 
 fun mk_terms ctxt qs result =
   let
     val ps = filter (fn (_, (\<^const_name>\<open>All\<close>, _)) => true | _ => false) (map_index I qs)
   in
     map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
     |> map (apsnd post_process)
   end
 
 fun test_term ctxt catch_code_errors (t, _) =
   let
     fun dest_result (Quickcheck.Result r) = r
     val opts =
       ((Config.get ctxt Quickcheck.genuine_only,
        (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
         Config.get ctxt Quickcheck.size)
     val thy = Proof_Context.theory_of ctxt
     val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
     val pnf_t = make_pnf_term thy t'
   in
     if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
       let
         fun wrap f (qs, t) =
           let val (qs1, qs2) = split_list qs
           in apfst (map2 pair qs1) (f (qs2, t)) end
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
         val act = if catch_code_errors then try else (fn f => SOME o f)
         val execute =
           dynamic_value_strict (true, opts)
             ((K true, fn _ => error ""),
               (get_existential_counterexample, put_existential_counterexample,
                 "Narrowing_Generators.put_existential_counterexample"))
             ctxt (apfst o Option.map o map_counterexample)
       in
         (case act execute (mk_property qs prop_t) of
           SOME (counterexample, result) => Quickcheck.Result
             {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
             evaluation_terms = Option.map (K []) counterexample,
             timings = #timings (dest_result result), reports = #reports (dest_result result)}
         | NONE =>
           (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
            Quickcheck.empty_result))
       end
     else
       let
         val frees = Term.add_frees t []
         val t' = fold_rev absfree frees t
         fun wrap f t = uncurry (fold_rev Term.abs) (f (strip_abs t))
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
           Const (\<^const_name>\<open>Quickcheck_Narrowing.ensure_testable\<close>,
             fastype_of t --> fastype_of t) $ t
         fun is_genuine (SOME (true, _)) = true
           | is_genuine _ = false
         val counterexample_of =
           Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
         val act = if catch_code_errors then try else (fn f => SOME o f)
         val execute =
           dynamic_value_strict (false, opts)
             ((is_genuine, counterexample_of),
               (get_counterexample, put_counterexample,
                 "Narrowing_Generators.put_counterexample"))
             ctxt (apfst o Option.map o apsnd o map)
       in
         (case act execute (ensure_testable (finitize t')) of
           SOME (counterexample, result) =>
             Quickcheck.Result
              {counterexample = counterexample_of counterexample,
               evaluation_terms = Option.map (K []) counterexample,
               timings = #timings (dest_result result),
               reports = #reports (dest_result result)}
         | NONE =>
           (Quickcheck.message ctxt "Conjecture is not executable with Quickcheck-narrowing";
            Quickcheck.empty_result))
       end
   end
 
 fun test_goals ctxt catch_code_errors insts goals =
   if not (getenv "ISABELLE_GHC" = "") then
     let
       val _ = Quickcheck.message ctxt "Testing conjecture with Quickcheck-narrowing..."
       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
     in
       Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
         (maps (map snd) correct_inst_goals) []
     end
   else
     (if Config.get ctxt Quickcheck.quiet then () else writeln
       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
         ^ "this variable to your GHC Haskell compiler in your settings file. "
         ^ "To deactivate narrowing-based quickcheck, set quickcheck_narrowing_active to false.");
       [Quickcheck.empty_result])
 
 
 (* setup *)
 
 val active = Attrib.setup_config_bool \<^binding>\<open>quickcheck_narrowing_active\<close> (K false)
 
 val _ =
   Theory.setup
    (Code.datatype_interpretation ensure_partial_term_of
     #> Code.datatype_interpretation ensure_partial_term_of_code
     #> Quickcheck_Common.datatype_interpretation \<^plugin>\<open>quickcheck_narrowing\<close>
       (\<^sort>\<open>narrowing\<close>, instantiate_narrowing_datatype)
     #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))))
 
 end
diff --git a/src/Pure/General/file.ML b/src/Pure/General/file.ML
--- a/src/Pure/General/file.ML
+++ b/src/Pure/General/file.ML
@@ -1,186 +1,184 @@
 (*  Title:      Pure/General/file.ML
     Author:     Makarius
 
 File-system operations.
 *)
 
 signature FILE =
 sig
   val standard_path: Path.T -> string
   val platform_path: Path.T -> string
   val bash_path: Path.T -> string
   val bash_paths: Path.T list -> string
   val bash_platform_path: Path.T -> string
   val absolute_path: Path.T -> Path.T
   val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool
   val is_file: Path.T -> bool
   val check_dir: Path.T -> Path.T
   val check_file: Path.T -> Path.T
   val open_dir: (OS.FileSys.dirstream -> 'a) -> Path.T -> 'a
   val open_input: (BinIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (BinIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (BinIO.outstream -> 'a) -> Path.T -> 'a
   val fold_dir: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_dir: Path.T -> string list
   val input: BinIO.instream -> string
   val input_size: int -> BinIO.instream -> string
   val input_all: BinIO.instream -> string
   val fold_lines: (string -> 'a -> 'a) -> Path.T -> 'a -> 'a
   val read_lines: Path.T -> string list
   val read: Path.T -> string
   val write: Path.T -> string -> unit
   val append: Path.T -> string -> unit
-  val generate: Path.T -> string -> unit
   val output: BinIO.outstream -> string -> unit
   val outputs: BinIO.outstream -> string list -> unit
   val write_list: Path.T -> string list -> unit
   val append_list: Path.T -> string list -> unit
   val write_buffer: Path.T -> Buffer.T -> unit
   val eq: Path.T * Path.T -> bool
 end;
 
 structure File: FILE =
 struct
 
 (* system path representations *)
 
 val standard_path = Path.implode o Path.expand;
 val platform_path = ML_System.platform_path o standard_path;
 
 val bash_path = Bash.string o standard_path;
 val bash_paths = Bash.strings o map standard_path;
 
 val bash_platform_path = Bash.string o platform_path;
 
 
 (* full_path *)
 
 val absolute_path =
   Path.expand #> (fn path =>
     if Path.is_absolute path then path
     else Path.explode (ML_System.standard_path (OS.FileSys.getDir ())) + path);
 
 fun full_path dir path =
   let
     val path' = Path.expand path;
     val _ = Path.is_current path' andalso error "Bad file specification";
   in absolute_path (dir + path') end;
 
 
 (* tmp_path *)
 
 fun tmp_path path = Path.variable "ISABELLE_TMP" + Path.base path;
 
 
 (* directory entries *)
 
 val exists = can OS.FileSys.modTime o platform_path;
 
 val rm = OS.FileSys.remove o platform_path;
 
 fun test_dir path = the_default false (try OS.FileSys.isDir (platform_path path));
 fun is_dir path = exists path andalso test_dir path;
 fun is_file path = exists path andalso not (test_dir path);
 
 fun check_dir path =
   if is_dir path then path
   else error ("No such directory: " ^ Path.print (Path.expand path));
 
 fun check_file path =
   if is_file path then path
   else error ("No such file: " ^ Path.print (Path.expand path));
 
 
 (* open streams *)
 
 local
 
 fun with_file open_file close_file f =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn path =>
     let
       val file = open_file path;
       val result = Exn.capture (restore_attributes f) file;
     in close_file file; Exn.release result end);
 
 in
 
 fun open_dir f = with_file OS.FileSys.openDir OS.FileSys.closeDir f o platform_path;
 fun open_input f = with_file BinIO.openIn BinIO.closeIn f o platform_path;
 fun open_output f = with_file BinIO.openOut BinIO.closeOut f o platform_path;
 fun open_append f = with_file BinIO.openAppend BinIO.closeOut f o platform_path;
 
 end;
 
 
 (* directory content *)
 
 fun fold_dir f path a =
   check_dir path |> open_dir (fn stream =>
     let
       fun read x =
         (case OS.FileSys.readDir stream of
           NONE => x
         | SOME entry => read (f entry x));
     in read a end);
 
 fun read_dir path = sort_strings (fold_dir cons path []);
 
 
 (* input *)
 
 val input = Byte.bytesToString o BinIO.input;
 fun input_size n stream = Byte.bytesToString (BinIO.inputN (stream, n));
 val input_all = Byte.bytesToString o BinIO.inputAll;
 
 (*
   scalable iterator:
   . avoid size limit of TextIO.inputAll and overhead of many TextIO.inputLine
   . optional terminator at end-of-input
 *)
 fun fold_lines f path a = open_input (fn file =>
   let
     fun read buf x =
       (case input file of
         "" => (case Buffer.content buf of "" => x | line => f line x)
       | input =>
           (case String.fields (fn c => c = #"\n") input of
             [rest] => read (Buffer.add rest buf) x
           | line :: more => read_more more (f (Buffer.content (Buffer.add line buf)) x)))
     and read_more [rest] x = read (Buffer.add rest Buffer.empty) x
       | read_more (line :: more) x = read_more more (f line x);
   in read Buffer.empty a end) path;
 
 fun read_lines path = rev (fold_lines cons path []);
 
 val read = open_input input_all;
 
 
 (* output *)
 
 fun output file txt = BinIO.output (file, Byte.stringToBytes txt);
 val outputs = List.app o output;
 
 fun output_list txts file = List.app (output file) txts;
 fun write_list path txts = open_output (output_list txts) path;
 fun append_list path txts = open_append (output_list txts) path;
 
 fun write path txt = write_list path [txt];
 fun append path txt = append_list path [txt];
-fun generate path txt = if try read path = SOME txt then () else write path txt;
 
 fun write_buffer path buf =
   open_output (fn file => List.app (output file) (Buffer.contents buf)) path;
 
 
 (* eq *)
 
 fun eq paths =
   (case try (apply2 (OS.FileSys.fileId o platform_path)) paths of
     SOME ids => is_equal (OS.FileSys.compare ids)
   | NONE => false);
 
 end;
diff --git a/src/Pure/Thy/export.ML b/src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML
+++ b/src/Pure/Thy/export.ML
@@ -1,73 +1,73 @@
 (*  Title:      Pure/Thy/export.ML
     Author:     Makarius
 
 Manage theory exports: compressed blobs.
 *)
 
 signature EXPORT =
 sig
   val report_export: theory -> Path.binding -> unit
   type params =
     {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool}
   val export_params: params -> XML.body -> unit
   val export: theory -> Path.binding -> XML.body -> unit
   val export_executable: theory -> Path.binding -> XML.body -> unit
   val export_file: theory -> Path.binding -> Path.T -> unit
   val export_executable_file: theory -> Path.binding -> Path.T -> unit
   val markup: theory -> Path.T -> Markup.T
   val message: theory -> Path.T -> string
 end;
 
 structure Export: EXPORT =
 struct
 
 (* export *)
 
 fun report_export thy binding =
   let
     val theory_name = Context.theory_long_name thy;
     val (path, pos) = Path.dest_binding binding;
     val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
   in Context_Position.report_generic (Context.Theory thy) pos markup end;
 
 type params =
   {theory: theory, binding: Path.binding, executable: bool, compress: bool, strict: bool};
 
 fun export_params ({theory = thy, binding, executable, compress, strict}: params) body =
  (report_export thy binding;
   (Output.try_protocol_message o Markup.export)
    {id = Position.id_of (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
     name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress,
     strict = strict} [body]);
 
 fun export thy binding body =
   export_params
     {theory = thy, binding = binding, executable = false, compress = true, strict = true} body;
 
 fun export_executable thy binding body =
   export_params
     {theory = thy, binding = binding, executable = true, compress = true, strict = true} body;
 
 fun export_file thy binding file =
-  export thy binding [XML.Text (File.read file)];
+  export thy binding (Bytes.contents_blob (Bytes.read file));
 
 fun export_executable_file thy binding file =
-  export_executable thy binding [XML.Text (File.read file)];
+  export_executable thy binding (Bytes.contents_blob (Bytes.read file));
 
 
 (* information message *)
 
 fun markup thy path =
   let
     val thy_path = Path.basic (Context.theory_long_name thy) + path;
     val name = (Markup.nameN, Path.implode thy_path);
   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
 fun message thy path =
   "See " ^ Markup.markup (markup thy path) "theory exports";
 
 end;
diff --git a/src/Pure/Tools/generated_files.ML b/src/Pure/Tools/generated_files.ML
--- a/src/Pure/Tools/generated_files.ML
+++ b/src/Pure/Tools/generated_files.ML
@@ -1,396 +1,401 @@
 (*  Title:      Pure/Tools/generated_files.ML
     Author:     Makarius
 
 Generated source files for other languages: with antiquotations, without Isabelle symbols.
 *)
 
 signature GENERATED_FILES =
 sig
-  val add_files: Path.binding * string -> theory -> theory
-  type file = {path: Path.T, pos: Position.T, content: string}
+  val add_files: Path.binding * Bytes.T -> theory -> theory
+  type file = {path: Path.T, pos: Position.T, content: Bytes.T}
   val file_binding: file -> Path.binding
   val file_markup: file -> Markup.T
   val print_file: file -> string
   val report_file: Proof.context -> Position.T -> file -> unit
   val get_files: theory -> file list
   val get_file: theory -> Path.binding -> file
   val get_files_in: Path.binding list * theory -> (file * Position.T) list
   val check_files_in: Proof.context ->
     (string * Position.T) list * (string * Position.T) option -> Path.binding list * theory
   val write_file: Path.T -> file -> unit
   val export_file: theory -> file -> unit
   type file_type =
     {name: string, ext: string, make_comment: string -> string, make_string: string -> string}
   val file_type:
     binding -> {ext: string, make_comment: string -> string, make_string: string -> string} ->
     theory -> theory
   val antiquotation: binding -> 'a Token.context_parser ->
     ({context: Proof.context, source: Token.src, file_type: file_type, argument: 'a} -> string) ->
     theory -> theory
   val set_string: string -> Proof.context -> Proof.context
   val generate_file: Path.binding * Input.source -> Proof.context -> local_theory
   val generate_file_cmd: (string * Position.T) * Input.source -> local_theory -> local_theory
   val export_generated_files: Proof.context -> (Path.binding list * theory) list -> unit
   val export_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list -> unit
   val with_compile_dir: (Path.T -> unit) -> unit
   val compile_generated_files: Proof.context ->
     (Path.binding list * theory) list ->
     (Path.T list * Path.T) list ->
     (Path.binding list * bool option) list ->
     Path.binding -> Input.source -> unit
   val compile_generated_files_cmd: Proof.context ->
     ((string * Position.T) list * (string * Position.T) option) list ->
     (Input.source list * Input.source) list ->
     ((string * Position.T) list * bool option) list ->
     string * Position.T -> Input.source -> unit
   val execute: Path.T -> Input.source -> string -> string
 end;
 
 structure Generated_Files: GENERATED_FILES =
 struct
 
 (** context data **)
 
-type file = Path.T * (Position.T * string);
+type file = Path.T * (Position.T * Bytes.T);
 
 type file_type =
   {name: string, ext: string, make_comment: string -> string, make_string: string -> string};
 
 type antiquotation = Token.src -> Proof.context -> file_type -> string;
 
 fun err_dup_files path pos pos' =
   error ("Duplicate generated file: " ^ Path.print path ^ Position.here_list [pos, pos']);
 
 structure Data = Theory_Data
 (
   type T =
     file list Symtab.table *  (*files for named theory*)
     file_type Name_Space.table *  (*file types*)
     antiquotation Name_Space.table;  (*antiquotations*)
   val empty =
     (Symtab.empty,
      Name_Space.empty_table Markup.file_typeN,
      Name_Space.empty_table Markup.antiquotationN);
   fun merge ((files1, types1, antiqs1), (files2, types2, antiqs2)) =
     let
       val files' =
-        (files1, files2) |> Symtab.join (K (Library.merge (fn ((path1, file1), (path2, file2)) =>
-          if path1 <> path2 then false
-          else if file1 = file2 then true
-          else err_dup_files path1 (#1 file1) (#1 file2))));
+        (files1, files2) |> Symtab.join (fn _ =>
+          Library.merge (fn ((path1, (pos1, bytes1)), (path2, (pos2, bytes2))) =>
+            if path1 <> path2 then false
+            else if pos1 = pos2 andalso Bytes.eq (bytes1, bytes2) then true
+            else err_dup_files path1 pos1 pos2));
       val types' = Name_Space.merge_tables (types1, types2);
       val antiqs' = Name_Space.merge_tables (antiqs1, antiqs2);
     in (files', types', antiqs') end;
 );
 
 fun lookup_files thy =
   Symtab.lookup_list (#1 (Data.get thy)) (Context.theory_long_name thy);
 
 fun update_files thy_files' thy =
   (Data.map o @{apply 3(1)}) (Symtab.update (Context.theory_long_name thy, thy_files')) thy;
 
 fun add_files (binding, content) thy =
   let
     val _ = Path.proper_binding binding;
     val (path, pos) = Path.dest_binding binding;
     val thy_files = lookup_files thy;
     val thy_files' =
       (case AList.lookup (op =) thy_files path of
         SOME (pos', _) => err_dup_files path pos pos'
       | NONE => (path, (pos, content)) :: thy_files);
   in update_files thy_files' thy end;
 
 
 (* get files *)
 
-type file = {path: Path.T, pos: Position.T, content: string};
+type file = {path: Path.T, pos: Position.T, content: Bytes.T};
 
 fun file_binding (file: file) = Path.binding (#path file, #pos file);
 
 fun file_markup (file: file) = (Markup.entityN, Position.def_properties_of (#pos file));
 
 fun print_file (file: file) = Markup.markup (file_markup file) (quote (Path.implode (#path file)));
 
 fun report_file ctxt pos file = Context_Position.report ctxt pos (file_markup file);
 
 
 fun get_files thy =
   lookup_files thy |> rev |> map (fn (path, (pos, content)) =>
     {path = path, pos = pos, content = content}: file);
 
 fun get_file thy binding =
   let val (path, pos) = Path.dest_binding binding in
     (case find_first (fn file => #path file = path) (get_files thy) of
       SOME file => file
     | NONE =>
         error ("Missing generated file " ^ Path.print path ^
           " in theory " ^ quote (Context.theory_long_name thy) ^ Position.here pos))
   end;
 
 fun get_files_in ([], thy) = map (rpair Position.none) (get_files thy)
   | get_files_in (files, thy) =
       map (fn binding => (get_file thy binding, Path.pos_of_binding binding)) files;
 
 
 (* check and output files *)
 
 fun check_files_in ctxt (files, opt_thy) =
   let
     val thy =
       (case opt_thy of
         SOME name => Theory.check {long = false} ctxt name
       | NONE => Proof_Context.theory_of ctxt);
   in (map Path.explode_binding files, thy) end;
 
 fun write_file dir (file: file) =
   let
     val path = Path.expand (dir + #path file);
     val _ = Isabelle_System.make_directory (Path.dir path);
-    val _ = File.generate path (#content file);
-  in () end;
+    val content = #content file;
+    val write_content =
+      (case try Bytes.read path of
+        SOME old_content => not (Bytes.eq (content, old_content))
+      | NONE => true)
+  in if write_content then Bytes.write path content else () end;
 
 fun export_file thy (file: file) =
-  Export.export thy (file_binding file) [XML.Text (#content file)];
+  Export.export thy (file_binding file) (Bytes.contents_blob (#content file));
 
 
 (* file types *)
 
 fun get_file_type thy ext =
   if ext = "" then error "Bad file extension"
   else
     (#2 (Data.get thy), NONE) |-> Name_Space.fold_table
       (fn (_, file_type) => fn res =>
         if #ext file_type = ext then SOME file_type else res)
     |> (fn SOME file_type => file_type
          | NONE => error ("Unknown file type for extension " ^ quote ext));
 
 fun file_type binding {ext, make_comment, make_string} thy =
   let
     val name = Binding.name_of binding;
     val pos = Binding.pos_of binding;
     val file_type = {name = name, ext = ext, make_comment = make_comment, make_string = make_string};
 
     val table = #2 (Data.get thy);
     val space = Name_Space.space_of_table table;
     val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
     val (_, data') = table |> Name_Space.define context true (Binding.make (name, pos), file_type);
 
     val _ =
       (case try (#name o get_file_type thy) ext of
         NONE => ()
       | SOME name' =>
           error ("Extension " ^ quote ext ^ " already registered for file type " ^
             quote (Markup.markup (Name_Space.markup space name') name') ^ Position.here pos));
   in thy |> (Data.map o @{apply 3(2)}) (K data') end;
 
 
 (* antiquotations *)
 
 val get_antiquotations = #3 o Data.get o Proof_Context.theory_of;
 
 fun antiquotation name scan body thy =
   let
     fun ant src ctxt file_type : string =
       let val (x, ctxt') = Token.syntax scan src ctxt
       in body {context = ctxt', source = src, file_type = file_type, argument = x} end;
   in
     thy
     |> (Data.map o @{apply 3(3)}) (Name_Space.define (Context.Theory thy) true (name, ant) #> #2)
   end;
 
 val scan_antiq =
   Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
 
 fun read_source ctxt (file_type: file_type) source =
   let
     val _ =
       Context_Position.report ctxt (Input.pos_of source)
         (Markup.language
           {name = #name file_type, symbols = false, antiquotes = true,
             delimited = Input.is_delimited source});
 
     val (input, _) =
       Input.source_explode source
       |> Scan.error (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_antiq));
 
     val _ = Context_Position.reports ctxt (Antiquote.antiq_reports input);
 
     fun expand antiq =
       (case antiq of
         Antiquote.Text s => s
       | Antiquote.Control {name, body, ...} =>
           let
             val src = Token.make_src name (if null body then [] else [Token.read_cartouche body]);
             val (src', ant) = Token.check_src ctxt get_antiquotations src;
           in ant src' ctxt file_type end
       | Antiquote.Antiq antiq => error ("Bad antiquotation " ^ Position.here (#1 (#range antiq))));
   in implode (map expand input) end;
 
 
 
 (** Isar commands **)
 
 (* generate_file *)
 
 fun generate_file (binding, source) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
 
     val (path, pos) = Path.dest_binding binding;
     val file_type =
       get_file_type thy (#2 (Path.split_ext path))
         handle ERROR msg => error (msg ^ Position.here pos);
 
     val header = #make_comment file_type " generated by Isabelle ";
-    val content = header ^ "\n" ^ read_source lthy file_type source;
+    val content = Bytes.string (header ^ "\n" ^ read_source lthy file_type source);
   in lthy |> (Local_Theory.background_theory o add_files) (binding, content) end;
 
 fun generate_file_cmd (file, source) lthy =
   generate_file (Path.explode_binding file, source) lthy;
 
 
 (* export_generated_files *)
 
 fun export_generated_files ctxt args =
   let val thy = Proof_Context.theory_of ctxt in
     (case map #1 (maps get_files_in args) of
       [] => ()
     | files =>
        (List.app (export_file thy) files;
         writeln (Export.message thy Path.current);
         writeln (cat_lines (map (prefix "  " o print_file) files))))
   end;
 
 fun export_generated_files_cmd ctxt args =
   export_generated_files ctxt (map (check_files_in ctxt) args);
 
 
 (* compile_generated_files *)
 
 val compile_dir = Config.declare_string ("compile_dir", \<^here>) (K "");
 
 fun with_compile_dir body : unit =
   body (Path.explode (Config.get (Context.the_local_context ()) compile_dir));
 
 fun compile_generated_files ctxt args external export export_prefix source =
   Isabelle_System.with_tmp_dir "compile" (fn dir =>
     let
       val thy = Proof_Context.theory_of ctxt;
 
       val files = maps get_files_in args;
       val _ = List.app (fn (file, pos) => report_file ctxt pos file) files;
       val _ = List.app (write_file dir o #1) files;
       val _ =
         external |> List.app (fn (files, base_dir) =>
           files |> List.app (fn file => Isabelle_System.copy_file_base (base_dir, file) dir));
       val _ =
         ML_Context.eval_in (SOME (Config.put compile_dir (Path.implode dir) ctxt))
           ML_Compiler.flags (Input.pos_of source)
           (ML_Lex.read "Generated_Files.with_compile_dir (" @
             ML_Lex.read_source source @ ML_Lex.read ")");
       val _ =
         export |> List.app (fn (bindings, executable) =>
           bindings |> List.app (fn binding0 =>
             let
               val binding = binding0 |> Path.map_binding (executable = SOME true ? Path.exe);
               val (path, pos) = Path.dest_binding binding;
               val content =
-                (case try File.read (dir + path) of
-                  SOME context => context
+                (case try Bytes.read (dir + path) of
+                  SOME bytes => Bytes.contents_blob bytes
                 | NONE => error ("Missing result file " ^ Path.print path ^ Position.here pos));
               val _ = Export.report_export thy export_prefix;
               val binding' =
                 Path.map_binding (Path.append (Path.path_of_binding export_prefix)) binding;
             in
               (if is_some executable then Export.export_executable else Export.export)
-                thy binding' [XML.Text content]
+                thy binding' content
             end));
       val _ =
         if null export then ()
         else writeln (Export.message thy (Path.path_of_binding export_prefix));
     in () end);
 
 fun compile_generated_files_cmd ctxt args external export export_prefix source =
   compile_generated_files ctxt
     (map (check_files_in ctxt) args)
     (external |> map (fn (raw_files, raw_base_dir) =>
       let
         val base_dir = Resources.check_dir ctxt NONE raw_base_dir;
         fun check source =
          (Resources.check_file ctxt (SOME base_dir) source;
           Path.explode (Input.string_of source));
         val files = map check raw_files;
       in (files, base_dir) end))
     ((map o apfst o map) Path.explode_binding export)
     (Path.explode_binding export_prefix)
     source;
 
 
 (* execute compiler -- auxiliary *)
 
 fun execute dir title compile =
   Isabelle_System.bash_process (Bash.script compile |> Bash.cwd dir)
   |> Process_Result.check
   |> Process_Result.out
     handle ERROR msg =>
       let val (s, pos) = Input.source_content title
       in error (s ^ " failed" ^ Position.here pos ^ ":\n" ^ msg) end;
 
 
 
 (** concrete file types **)
 
 val _ =
   Theory.setup
     (file_type \<^binding>\<open>Haskell\<close>
       {ext = "hs",
        make_comment = enclose "{-" "-}",
        make_string = GHC.print_string});
 
 
 
 (** concrete antiquotations **)
 
 (* ML expression as string literal *)
 
 structure Local_Data = Proof_Data
 (
   type T = string option;
   fun init _ = NONE;
 );
 
 val set_string = Local_Data.put o SOME;
 
 fun the_string ctxt =
   (case Local_Data.get ctxt of
     SOME s => s
   | NONE => raise Fail "No result string");
 
 val _ =
   Theory.setup
     (antiquotation \<^binding>\<open>cartouche\<close> (Scan.lift Args.cartouche_input)
       (fn {context = ctxt, file_type, argument, ...} =>
         ctxt |> Context.proof_map
           (ML_Context.expression (Input.pos_of argument)
             (ML_Lex.read "Theory.local_setup (Generated_Files.set_string (" @
              ML_Lex.read_source argument @ ML_Lex.read "))"))
         |> the_string |> #make_string file_type));
 
 
 (* file-system paths *)
 
 fun path_antiquotation binding check =
   antiquotation binding
     (Args.context -- Scan.lift Parse.path_input >>
       (fn (ctxt, source) => (check ctxt (SOME Path.current) source |> Path.implode)))
     (fn {file_type, argument, ...} => #make_string file_type argument);
 
 val _ =
   Theory.setup
    (path_antiquotation \<^binding>\<open>path\<close> Resources.check_path #>
     path_antiquotation \<^binding>\<open>file\<close> Resources.check_file #>
     path_antiquotation \<^binding>\<open>dir\<close> Resources.check_dir);
 
 end;
diff --git a/src/Tools/Code/code_printer.ML b/src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML
+++ b/src/Tools/Code/code_printer.ML
@@ -1,448 +1,448 @@
 (*  Title:      Tools/Code/code_printer.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Generic operations for pretty printing of target language code.
 *)
 
 signature CODE_PRINTER =
 sig
   type itype = Code_Thingol.itype
   type iterm = Code_Thingol.iterm
   type const = Code_Thingol.const
   type dict = Code_Thingol.dict
 
   val eqn_error: theory -> thm option -> string -> 'a
 
   val @@ : 'a * 'a -> 'a list
   val @| : 'a list * 'a -> 'a list
   val str: string -> Pretty.T
   val concat: Pretty.T list -> Pretty.T
   val brackets: Pretty.T list -> Pretty.T
   val enclose: string -> string -> Pretty.T list -> Pretty.T
   val commas: Pretty.T list -> Pretty.T list
   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
   val semicolon: Pretty.T list -> Pretty.T
   val doublesemicolon: Pretty.T list -> Pretty.T
   val indent: int -> Pretty.T -> Pretty.T
   val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
-  val format: Code_Symbol.T list -> int -> Pretty.T -> string
+  val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T
 
   type var_ctxt
   val make_vars: string list -> var_ctxt
   val intro_vars: string list -> var_ctxt -> var_ctxt
   val lookup_var: var_ctxt -> string -> string
   val intro_base_names: (string -> bool) -> (string -> string)
     -> string list -> var_ctxt -> var_ctxt
   val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
     -> iterm list -> var_ctxt -> var_ctxt
   val aux_params: var_ctxt -> iterm list list -> string list
 
   type literals
   val Literals: { literal_string: string -> string,
         literal_numeral: int -> string,
         literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
     -> literals
   val literal_string: literals -> string -> string
   val literal_numeral: literals -> int -> string
   val literal_list: literals -> Pretty.T list -> Pretty.T
   val infix_cons: literals -> int * string
 
   type lrx
   val L: lrx
   val R: lrx
   val X: lrx
   type fixity
   val BR: fixity
   val NOBR: fixity
   val INFX: int * lrx -> fixity
   val APP: fixity
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
   val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
   type raw_const_syntax
   val plain_const_syntax: string -> raw_const_syntax
   type simple_const_syntax
   val simple_const_syntax: simple_const_syntax -> raw_const_syntax
   type complex_const_syntax
   val complex_const_syntax: complex_const_syntax -> raw_const_syntax
   val parse_const_syntax: raw_const_syntax parser
   val requires_args: raw_const_syntax -> int
   datatype const_printer = Plain_printer of string
     | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
         -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
   type const_syntax = int * const_printer
   val prep_const_syntax: theory -> literals
     -> string -> raw_const_syntax -> const_syntax
   type tyco_syntax
   val parse_tyco_syntax: tyco_syntax parser
   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> fixity
     -> iterm -> var_ctxt -> Pretty.T * var_ctxt
 
   type identifiers
   type printings
   type data
   val empty_data: data
   val map_data: (string list * identifiers * printings
     -> string list * identifiers * printings)
     -> data -> data
   val merge_data: data * data -> data
   val the_reserved: data -> string list;
   val the_identifiers: data -> identifiers;
   val the_printings: data -> printings;
 end;
 
 structure Code_Printer : CODE_PRINTER =
 struct
 
 open Basic_Code_Symbol;
 open Code_Thingol;
 
 (** generic nonsense *)
 
 fun eqn_error thy (SOME thm) s =
       error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
   | eqn_error _ NONE s = error s;
 
 val code_presentationN = "code_presentation";
 val stmt_nameN = "stmt_name";
 val _ = Markup.add_mode code_presentationN YXML.output_markup;
 
 
 (** assembling and printing text pieces **)
 
 infixr 5 @@;
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
 fun with_no_print_mode f = Print_Mode.setmp [] f;
 val str = with_no_print_mode Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
 val commas = with_no_print_mode Pretty.commas;
 fun enclose l r = with_no_print_mode (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
 fun enum sep l r = with_no_print_mode (Pretty.enum sep l r);
 fun enum_default default sep l r [] = str default
   | enum_default default sep l r xs = enum sep l r xs;
 fun semicolon ps = Pretty.block [concat ps, str ";"];
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
 fun indent i = with_no_print_mode (Pretty.indent i);
 
 fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f;
 
 fun markup_stmt sym = with_presentation_marker
   (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
 
 fun filter_presentation [] xml =
       Buffer.build (fold XML.add_content xml)
   | filter_presentation presentation_syms xml =
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
         fun is_selected (name, attrs) =
           name = code_presentationN
           andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
         fun add_content_with_space tree (is_first, buf) =
           buf
           |> not is_first ? Buffer.add "\n\n"
           |> XML.add_content tree
           |> pair false;
         fun filter (XML.Elem (name_attrs, xs)) =
               fold (if is_selected name_attrs then add_content_with_space else filter) xs
           | filter (XML.Text _) = I;
       in snd (fold filter xml (true, Buffer.empty)) end;
 
 fun format presentation_names width =
   with_presentation_marker (Pretty.string_of_margin width)
   #> YXML.parse_body
   #> filter_presentation presentation_names
   #> Buffer.add "\n"
-  #> Buffer.content;
+  #> Bytes.buffer;
 
 
 (** names and variable name contexts **)
 
 type var_ctxt = string Symtab.table * Name.context;
 
 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
   Name.make_context names);
 
 fun intro_vars names (namemap, namectxt) =
   let
     val (names', namectxt') = fold_map Name.variant names namectxt;
     val namemap' = fold2 (curry Symtab.update) names names' namemap;
   in (namemap', namectxt') end;
 
 fun lookup_var (namemap, _) name =
   case Symtab.lookup namemap name of
     SOME name' => name'
   | NONE => error ("Invalid name in context: " ^ quote name);
 
 fun aux_params vars lhss =
   let
     fun fish_param _ (w as SOME _) = w
       | fish_param (IVar (SOME v)) NONE = SOME v
       | fish_param _ NONE = NONE;
     fun fillup_param _ (_, SOME v) = v
       | fillup_param x (i, NONE) = x ^ string_of_int i;
     val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
     val x = singleton (Name.variant_list (map_filter I fished1)) "x";
     val fished2 = map_index (fillup_param x) fished1;
     val (fished3, _) = fold_map Name.variant fished2 Name.context;
     val vars' = intro_vars fished3 vars;
   in map (lookup_var vars') fished3 end;
 
 fun intro_base_names no_syntax deresolve =
   map_filter (fn name => if no_syntax name then
       let val name' = deresolve name in
         if Long_Name.is_qualified name' then NONE else SOME name'
       end else NONE)
   #> intro_vars;
 
 fun intro_base_names_for no_syntax deresolve ts =
   []
   |> fold Code_Thingol.add_constsyms ts 
   |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
 
 
 (** pretty literals **)
 
 datatype literals = Literals of {
   literal_string: string -> string,
   literal_numeral: int -> string,
   literal_list: Pretty.T list -> Pretty.T,
   infix_cons: int * string
 };
 
 fun dest_Literals (Literals lits) = lits;
 
 val literal_string = #literal_string o dest_Literals;
 val literal_numeral = #literal_numeral o dest_Literals;
 val literal_list = #literal_list o dest_Literals;
 val infix_cons = #infix_cons o dest_Literals;
 
 
 (** syntax printer **)
 
 (* binding priorities *)
 
 datatype lrx = L | R | X;
 
 datatype fixity =
     BR
   | NOBR
   | INFX of (int * lrx);
 
 val APP = INFX (~1, L);
 
 fun fixity_lrx L L = false
   | fixity_lrx R R = false
   | fixity_lrx _ _ = true;
 
 fun fixity NOBR _ = false
   | fixity _ NOBR = false
   | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
       pr < pr_ctxt
       orelse pr = pr_ctxt
         andalso fixity_lrx lr lr_ctxt
       orelse pr_ctxt = ~1
   | fixity BR (INFX _) = false
   | fixity _ _ = true;
 
 fun gen_brackify _ [p] = p
   | gen_brackify true (ps as _::_) = enclose "(" ")" ps
   | gen_brackify false (ps as _::_) = Pretty.block ps;
 
 fun brackify fxy_ctxt =
   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
 
 fun brackify_infix infx fxy_ctxt (l, m, r) =
   gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
 
 fun brackify_block fxy_ctxt p1 ps p2 =
   let val p = Pretty.block_enclose (p1, p2) ps
   in if fixity BR fxy_ctxt
     then enclose "(" ")" [p]
     else p
   end;
 
 fun gen_applify strict opn cls f fxy_ctxt p [] =
       if strict
       then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)]
       else p
   | gen_applify strict opn cls f fxy_ctxt p ps =
       gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
 
 fun applify opn = gen_applify false opn;
 
 fun tuplify _ _ [] = NONE
   | tuplify print fxy [x] = SOME (print fxy x)
   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
 
 
 (* generic syntax *)
 
 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   -> fixity -> (iterm * itype) list -> Pretty.T);
 
 type complex_const_syntax = int * (literals
   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
 datatype raw_const_syntax = plain_const_syntax of string
   | complex_const_syntax of complex_const_syntax;
 
 fun simple_const_syntax syn =
   complex_const_syntax
     (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
 
 fun requires_args (plain_const_syntax _) = 0
   | requires_args (complex_const_syntax (k, _)) = k;
 
 datatype const_printer = Plain_printer of string
   | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
       -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
 
 type const_syntax = int * const_printer;
 
 fun prep_const_syntax thy literals c (plain_const_syntax s) =
       (Code.args_number thy c, Plain_printer s)
   | prep_const_syntax thy literals c (complex_const_syntax (n, f))=
       (n, Complex_printer (f literals));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     (app as ({ sym, dom, ... }, ts)) =
   case sym of
     Constant const => (case const_syntax const of
       NONE => brackify fxy (print_app_expr some_thm vars app)
     | SOME (_, Plain_printer s) =>
         brackify fxy (str s :: map (print_term some_thm vars BR) ts)
     | SOME (k, Complex_printer print) =>
         let
           fun print' fxy ts =
             print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
         in
           if k = length ts
           then print' fxy ts
           else if k < length ts
           then case chop k ts of (ts1, ts2) =>
             brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
           else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
         end)
   | _ => brackify fxy (print_app_expr some_thm vars app);
 
 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   let
     val vs = build (Code_Thingol.add_varnames pat);
     val vars' = intro_vars vs vars;
   in (print_term thm vars' fxy pat, vars') end;
 
 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   -> fixity -> itype list -> Pretty.T);
 
 
 (* mixfix syntax *)
 
 datatype 'a mixfix =
     Arg of fixity
   | String of string
   | Break;
 
 fun printer_of_mixfix prep_arg (fixity_this, mfx) =
   let
     fun is_arg (Arg _) = true
       | is_arg _ = false;
     val i = (length o filter is_arg) mfx;
     fun fillin _ [] [] =
           []
       | fillin print (Arg fxy :: mfx) (a :: args) =
           (print fxy o prep_arg) a :: fillin print mfx args
       | fillin print (String s :: mfx) args =
           str s :: fillin print mfx args
       | fillin print (Break :: mfx) args =
           Pretty.brk 1 :: fillin print mfx args;
   in
     (i, fn print => fn fixity_ctxt => fn args =>
       gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
   end;
 
 fun read_infix (fixity_this, i) s =
   let
     val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X);
     val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X);
   in
     (INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r])
   end;
 
 fun read_mixfix s =
   let
     val sym_any = Scan.one Symbol.not_eof;
     val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
       || ($$ "_" >> K (Arg BR))
       || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
       || (Scan.repeat1
            (   $$ "'" |-- sym_any
             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
                  sym_any) >> (String o implode)));
     fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
       | err _ (_, SOME msg) = msg;
   in
     case Scan.finite Symbol.stopper parse (Symbol.explode s) of
         (fixity_mixfix, []) => fixity_mixfix
       | _ => Scan.!! (err s) Scan.fail ()
   end;
 
 val parse_fixity =
   (\<^keyword>\<open>infix\<close> >> K X) || (\<^keyword>\<open>infixl\<close> >> K L) || (\<^keyword>\<open>infixr\<close> >> K R)
 
 fun parse_mixfix x =
   (Parse.string >> read_mixfix
   || parse_fixity -- Parse.nat -- Parse.string
      >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x;
 
 fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s
   | syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) =
       of_printer (printer_of_mixfix prep_arg (fixity, mfx));
 
 fun parse_tyco_syntax x =
   (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x;
 
 val parse_const_syntax =
   parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
 
 
 (** custom data structure **)
 
 type identifiers = (string list * string, string list * string, string list * string, string list * string,
   string list * string, string list * string) Code_Symbol.data;
 type printings = (const_syntax, tyco_syntax, string, unit, unit,
     (Pretty.T * Code_Symbol.T list)) Code_Symbol.data;
 
 datatype data = Data of { reserved: string list, identifiers: identifiers,
   printings: printings };
 
 fun make_data (reserved, identifiers, printings) =
   Data { reserved = reserved, identifiers = identifiers, printings = printings };
 val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
 fun map_data f (Data { reserved, identifiers, printings }) =
   make_data (f (reserved, identifiers, printings));
 fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
     Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
   make_data (merge (op =) (reserved1, reserved2),
     Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
 
 fun the_reserved (Data { reserved, ... }) = reserved;
 fun the_identifiers (Data { identifiers , ... }) = identifiers;
 fun the_printings (Data { printings, ... }) = printings;
 
 
 end; (*struct*)
diff --git a/src/Tools/Code/code_runtime.ML b/src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML
+++ b/src/Tools/Code/code_runtime.ML
@@ -1,885 +1,885 @@
 (*  Title:      Tools/Code/code_runtime.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Runtime services building on code generation into implementation language SML.
 *)
 
 signature CODE_RUNTIME =
 sig
   val target: string
   val value: Proof.context ->
     (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string ->
     string * string -> 'a
   type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string
   val dynamic_value: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a option
   val dynamic_value_strict: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
   val dynamic_value_exn: 'a cookie -> Proof.context -> string option
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
   val dynamic_holds_conv: Proof.context -> conv
   val code_reflect: (string * string list option) list -> string list -> string
     -> Path.binding option -> theory -> theory
   val code_reflect_cmd: (string * string list option) list -> string list -> string
     -> Path.binding option -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
   val mount_computation: Proof.context -> (string * typ) list -> typ
     -> (term -> 'ml) -> ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
   val mount_computation_conv: Proof.context -> (string * typ) list -> typ
     -> (term -> 'ml) -> (Proof.context -> 'ml -> conv) -> Proof.context -> conv
   val mount_computation_check: Proof.context -> (string * typ) list
     -> (term -> truth) -> Proof.context -> conv
   val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
   val trace: bool Config.T
 end;
 
 structure Code_Runtime : CODE_RUNTIME =
 struct
 
 open Basic_Code_Symbol;
 
 (** ML compiler as evaluation environment **)
 
 (* technical prerequisites *)
 
 val thisN = "Code_Runtime";
 val prefix_this = Long_Name.append thisN;
 val truthN = prefix_this "truth";
 val HoldsN = prefix_this "Holds";
 
 val target = "Eval";
 
 datatype truth = Holds;
 
 val _ = Theory.setup
   (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
   #> Code_Target.set_printings (Type_Constructor (\<^type_name>\<open>prop\<close>,
     [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))]))
   #> Code_Target.set_printings (Constant (\<^const_name>\<open>Code_Generator.holds\<close>,
     [(target, SOME (Code_Printer.plain_const_syntax HoldsN))]))
   #> Code_Target.add_reserved target thisN
   #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
        (*avoid further pervasive infix names*)
 
 val trace = Attrib.setup_config_bool \<^binding>\<open>code_runtime_trace\<close> (K false);
 
 fun compile_ML verbose code context =
  (if Config.get_generic context trace then tracing code else ();
   Code_Preproc.timed "compiling ML" Context.proof_of
     (ML_Context.exec (fn () => ML_Compiler0.ML ML_Env.context
     {line = 0, file = "generated code", verbose = verbose,
        debug = false} code)) context);
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
     val code =
       prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
       put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
     val ctxt' = ctxt
       |> put (fn () => error ("Bad compilation for " ^ quote put_ml))
       |> Context.proof_map (compile_ML false code);
     val computator = get ctxt';
   in Code_Preproc.timed_exec "running ML" computator ctxt' end;
 
 
 (* evaluation into ML language values *)
 
 type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
 
 fun reject_vars ctxt t =
   ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t);
 
 fun build_compilation_text ctxt some_target program consts =
   Code_Target.compilation_text ctxt (the_default target some_target) program consts false
-  #>> (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
+  #>> (fn ml_modules => space_implode "\n\n" (map (Bytes.content o snd) ml_modules));
 
 fun run_compilation_text cookie ctxt comp vs_t args =
   let
     val (program_code, value_name) = comp vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
   in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
 
 fun partiality_as_none e = SOME (Exn.release e)
   handle General.Match => NONE
     | General.Bind => NONE
     | General.Fail _ => NONE;
 
 fun dynamic_value_exn cookie ctxt some_target postproc t args =
   let
     val _ = reject_vars ctxt t;
     val _ = if Config.get ctxt trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
       else ()
     fun comp program _ vs_ty_t deps =
       run_compilation_text cookie ctxt (build_compilation_text ctxt some_target program deps) vs_ty_t args;
   in Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) comp t end;
 
 fun dynamic_value_strict cookie ctxt some_target postproc t args =
   Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args);
 
 fun dynamic_value cookie ctxt some_target postproc t args =
   partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
 
 
 (* evaluation for truth or nothing *)
 
 structure Truth_Result = Proof_Data
 (
   type T = unit -> truth;
   val empty: T = fn () => raise Fail "Truth_Result";
   fun init _ = empty;
 );
 val put_truth = Truth_Result.put;
 val truth_cookie = (Truth_Result.get, put_truth, prefix_this "put_truth");
 
 local
 
 val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of);
 
 fun check_holds ctxt evaluator vs_t ct =
   let
     val t = Thm.term_of ct;
     val _ = if fastype_of t <> propT
       then error ("Not a proposition: " ^ Syntax.string_of_term ctxt t)
       else ();
     val iff = Thm.cterm_of ctxt (Term.Const (\<^const_name>\<open>Pure.eq\<close>, propT --> propT --> propT));
     val result = case partiality_as_none (run_compilation_text truth_cookie ctxt evaluator vs_t [])
      of SOME Holds => true
       | _ => false;
   in
     Thm.mk_binop iff ct (if result then \<^cprop>\<open>PROP Code_Generator.holds\<close> else ct)
   end;
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>holds_by_evaluation\<close>,
   fn (ctxt, evaluator, vs_t, ct) => check_holds ctxt evaluator vs_t ct)));
 
 fun check_holds_oracle ctxt evaluator vs_ty_t ct =
   raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct);
 
 in
 
 fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt
   (fn program => fn vs_t => fn deps =>
     check_holds_oracle ctxt (build_compilation_text ctxt NONE program deps) vs_t)
       o reject_vars ctxt;
 
 end; (*local*)
 
 
 (** generator for computations -- partial implementations of the universal morphism from Isabelle to ML terms **)
 
 (* auxiliary *)
 
 val generated_computationN = "Generated_Computation";
 
 
 (* possible type signatures of constants *)
 
 fun typ_signatures' T =
   let
     val (Ts, T') = strip_type T;
   in map_range (fn n => (drop n Ts ---> T', take n Ts)) (length Ts + 1) end;
 
 fun typ_signatures cTs =
   let
     fun add (c, T) =
       fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts)))
         (typ_signatures' T);
   in
     Typtab.empty
     |> fold add cTs
     |> Typtab.lookup_list
   end;
 
 
 (* name mangling *)
 
 local
 
 fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco]
   | tycos_of _ = [];
 
 val ml_name_of = Name.desymbolize NONE o Long_Name.base_name;
 
 in
 
 val covered_constsN = "covered_consts";
 
 fun of_term_for_typ Ts =
   let
     val names = Ts
       |> map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of)
       |> Name.variant_list [];
   in the o AList.lookup (op =) (Ts ~~ names) end;
 
 fun eval_for_const ctxt cTs =
   let
     fun symbol_list (c, T) = c :: maps tycos_of (Sign.const_typargs (Proof_Context.theory_of ctxt) (c, T))
     val names = cTs
       |> map (prefix "eval_" o space_implode "_" o map ml_name_of o symbol_list)
       |> Name.variant_list [];
   in the o AList.lookup (op =) (cTs ~~ names) end;
 
 end;
 
 
 (* checks for input terms *)
 
 fun monomorphic T = fold_atyps ((K o K) false) T true;
 
 fun check_typ ctxt T t =
   Syntax.check_term ctxt (Type.constraint T t);
 
 fun check_computation_input ctxt cTs t =
   let
     fun check t = check_comb (strip_comb t)
     and check_comb (t as Abs _, _) =
           error ("Bad term, contains abstraction: " ^ Syntax.string_of_term ctxt t)
       | check_comb (t as Const (cT as (c, T)), ts) =
           let
             val _ = if not (member (op =) cTs cT)
               then error ("Bad term, computation cannot proceed on constant " ^ Syntax.string_of_term ctxt t)
               else ();
             val _ = if not (monomorphic T)
               then error ("Bad term, contains polymorphic constant " ^ Syntax.string_of_term ctxt t)
               else ();
             val _ = map check ts;
           in () end;
     val _ = check t;
   in t end;
 
 
 (* code generation for of the universal morphism *)
 
 val print_const = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_typ;
 
 fun print_of_term_funs { typ_signatures_for, eval_for_const, of_term_for_typ } Ts =
   let
     val var_names = map_range (fn n => "t" ^ string_of_int (n + 1));
     fun print_lhs c xs = "Const (" ^ quote c ^ ", _)"
       |> fold (fn x => fn s => s ^ " $ " ^ x) xs
       |> enclose "(" ")";
     fun print_rhs c Ts T xs = eval_for_const (c, Ts ---> T)
       |> fold2 (fn T' => fn x => fn s =>
          s ^ (" (" ^ of_term_for_typ T' ^ " " ^ x ^ ")")) Ts xs
     fun print_eq T (c, Ts) =
       let
         val xs = var_names (length Ts);
       in print_lhs c xs ^ " = " ^ print_rhs c Ts T xs end;
     fun print_eqs T =
       let
         val typ_signs = typ_signatures_for T;
         val name = of_term_for_typ T;
       in
         map (print_eq T) typ_signs
         |> map (prefix (name ^ " "))
         |> space_implode "\n  | "
       end;
   in
     map print_eqs Ts
     |> space_implode "\nand "
     |> prefix "fun "
   end;
 
 fun print_computation_code ctxt compiled_value [] requested_Ts =
       if null requested_Ts then ("", [])
       else error ("No equation available for requested type "
         ^ Syntax.string_of_typ ctxt (hd requested_Ts))
   | print_computation_code ctxt compiled_value cTs requested_Ts =
       let
         val proper_cTs = map_filter I cTs;
         val typ_signatures_for = typ_signatures proper_cTs;
         fun add_typ T Ts =
           if member (op =) Ts T
           then Ts
           else case typ_signatures_for T of
             [] => error ("No equation available for requested type "
               ^ Syntax.string_of_typ ctxt T)
           | typ_signs =>
               Ts
               |> cons T
               |> fold (fold add_typ o snd) typ_signs;
         val required_Ts = build (fold add_typ requested_Ts);
         val of_term_for_typ' = of_term_for_typ required_Ts;
         val eval_for_const' = eval_for_const ctxt proper_cTs;
         val eval_for_const'' = the_default "_" o Option.map eval_for_const';
         val eval_tuple = enclose "(" ")" (commas (map eval_for_const' proper_cTs));
         fun mk_abs s = "fn " ^ s ^ " => ";
         val eval_abs = space_implode ""
           (map (mk_abs o eval_for_const'') cTs);
         val of_term_code = print_of_term_funs {
           typ_signatures_for = typ_signatures_for,
           eval_for_const = eval_for_const',
           of_term_for_typ = of_term_for_typ' } required_Ts;
         val of_term_names = map (Long_Name.append generated_computationN
           o of_term_for_typ') requested_Ts;
       in
         cat_lines [
           "structure " ^ generated_computationN ^ " =",
           "struct",
           "",
           "val " ^ covered_constsN ^ " = " ^ ML_Syntax.print_list print_const proper_cTs ^ ";",
           "",
           "val " ^ eval_tuple ^ " = " ^ compiled_value ^ " ()",
           "  (" ^ eval_abs,
           "    " ^ eval_tuple ^ ");",
           "",
           of_term_code,
           "",
           "end"
         ] |> rpair of_term_names
       end;
 
 
 (* dedicated preprocessor for computations *)
 
 structure Computation_Preproc_Data = Theory_Data
 (
   type T = thm list;
   val empty = [];
   val merge = Library.merge Thm.eq_thm_prop;
 );
 
 local
 
 fun add thm thy =
   let
     val thms = Simplifier.mksimps (Proof_Context.init_global thy) thm;
   in
     thy
     |> Computation_Preproc_Data.map (fold (insert Thm.eq_thm_prop o Thm.trim_context) thms)
   end;
 
 fun get ctxt =
   Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
   |> map (Thm.transfer' ctxt)
 
 in
 
 fun preprocess_conv { ctxt } = 
   let
     val rules = get ctxt;
   in fn ctxt' => Raw_Simplifier.rewrite ctxt' false rules end;
 
 fun preprocess_term { ctxt } =
   let
     val rules = map (Logic.dest_equals o Thm.plain_prop_of) (get ctxt);
   in fn ctxt' => Pattern.rewrite_term (Proof_Context.theory_of ctxt') rules [] end;
 
 val _ = Theory.setup
   (Attrib.setup \<^binding>\<open>code_computation_unfold\<close>
     (Scan.succeed (Thm.declaration_attribute (fn thm => Context.mapping (add thm) I)))
     "preprocessing equations for computation");
 
 end;
 
 
 (* mounting computations *)
 
 fun prechecked_computation T raw_computation ctxt =
   check_typ ctxt T
   #> reject_vars ctxt
   #> raw_computation ctxt;
 
 fun prechecked_conv T raw_conv ctxt =
   tap (check_typ ctxt T o reject_vars ctxt o Thm.term_of)
   #> raw_conv ctxt;
 
 fun checked_computation cTs raw_computation ctxt =
   check_computation_input ctxt cTs
   #> Exn.interruptible_capture raw_computation
   #> partiality_as_none;
 
 fun mount_computation ctxt cTs T raw_computation lift_postproc =
   let
     val preprocess = preprocess_term { ctxt = ctxt };
     val computation = prechecked_computation T (Code_Preproc.static_value
       { ctxt = ctxt, lift_postproc = lift_postproc, consts = [] }
       (K (checked_computation cTs raw_computation)));
   in fn ctxt' => preprocess ctxt' #> computation ctxt' end;
 
 fun mount_computation_conv ctxt cTs T raw_computation conv =
   let
     val preprocess = preprocess_conv { ctxt = ctxt };
     val computation_conv = prechecked_conv T (Code_Preproc.static_conv
       { ctxt = ctxt, consts = [] }
       (K (fn ctxt' => fn t =>
         case checked_computation cTs raw_computation ctxt' t of
           SOME x => conv ctxt' x
         | NONE => Conv.all_conv)));
   in fn ctxt' => preprocess ctxt' then_conv computation_conv ctxt' end;
 
 local
 
 fun holds ct = Thm.mk_binop \<^cterm>\<open>Pure.eq :: prop \<Rightarrow> prop \<Rightarrow> prop\<close>
   ct \<^cprop>\<open>PROP Code_Generator.holds\<close>;
 
 val (_, holds_oracle) = Context.>>> (Context.map_theory_result
   (Thm.add_oracle (\<^binding>\<open>holds\<close>, holds)));
 
 in
 
 fun mount_computation_check ctxt cTs raw_computation =
   mount_computation_conv ctxt cTs \<^typ>\<open>prop\<close> raw_computation
     ((K o K) holds_oracle);
 
 end;
 
 
 (** variants of universal runtime code generation **)
 
 (*FIXME consolidate variants*)
 
 fun runtime_code'' ctxt module_name program tycos consts =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (ml_modules, target_names) =
       Code_Target.produce_code_for ctxt
         target module_name NONE [] program false (map Constant consts @ map Type_Constructor tycos);
-    val ml_code = space_implode "\n\n" (map snd ml_modules);
+    val ml_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
     val (consts', tycos') = chop (length consts) target_names;
     val consts_map = map2 (fn const =>
       fn NONE =>
           error ("Constant " ^ (quote o Code.string_of_const thy) const ^
             "\nhas a user-defined serialization")
        | SOME const' => (const, const')) consts consts'
     val tycos_map = map2 (fn tyco =>
       fn NONE =>
           error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
             "\nhas a user-defined serialization")
         | SOME tyco' => (tyco, tyco')) tycos tycos';
   in (ml_code, (tycos_map, consts_map)) end;
 
 fun runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun the_const (Const cT) = cT
       | the_const t = error ("No constant after preprocessing: " ^ Syntax.string_of_term ctxt t)
     val raw_computation_cTs = case evals of
         Abs (_, _, t) => (map the_const o snd o strip_comb) t
       | _ => error ("Bad term after preprocessing: " ^ Syntax.string_of_term ctxt evals);
     val computation_cTs = fold_rev (fn cT => fn cTs =>
       (if member (op =) cTs (SOME cT) then NONE else SOME cT) :: cTs) raw_computation_cTs [];
     val consts' = fold (fn NONE => I | SOME (c, _) => insert (op =) c)
       computation_cTs named_consts;
     val program' = Code_Thingol.consts_program ctxt consts';
       (*FIXME insufficient interfaces require double invocation of code generator*)
     val program'' = Code_Symbol.Graph.merge (K true) (program, program');
     val ((ml_modules, compiled_value), deresolve) =
       Code_Target.compilation_text' ctxt target some_module_name program''
         (map Code_Symbol.Type_Constructor named_tycos @ map Code_Symbol.Constant consts' @ deps) true vs_ty_evals;
         (*FIXME constrain signature*)
     fun deresolve_tyco tyco = case (deresolve o Code_Symbol.Type_Constructor) tyco of
           NONE => error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^
             "\nhas a user-defined serialization")
         | SOME c' => c';
     fun deresolve_const c = case (deresolve o Code_Symbol.Constant) c of
           NONE => error ("Constant " ^ (quote o Code.string_of_const thy) c ^
             "\nhas a user-defined serialization")
         | SOME c' => c';
     val tyco_names =  map deresolve_tyco named_tycos;
     val const_names = map deresolve_const named_consts;
-    val generated_code = space_implode "\n\n" (map snd ml_modules);
+    val generated_code = space_implode "\n\n" (map (Bytes.content o snd) ml_modules);
     val (of_term_code, of_term_names) =
       print_computation_code ctxt compiled_value computation_cTs computation_Ts;
     val compiled_computation = generated_code ^ "\n" ^ of_term_code;
   in
     compiled_computation
     |> rpair { tyco_map = named_tycos ~~ tyco_names,
       const_map = named_consts ~~ const_names,
       of_term_map = computation_Ts ~~ of_term_names }
   end;
 
 fun funs_of_maps { tyco_map, const_map, of_term_map } =
   { name_for_tyco = the o AList.lookup (op =) tyco_map,
     name_for_const = the o AList.lookup (op =) const_map,
     of_term_for_typ = the o AList.lookup (op =) of_term_map };
 
 fun runtime_code ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps =
   runtime_code' ctxt some_module_name named_tycos named_consts computation_Ts program evals vs_ty_evals deps
   ||> funs_of_maps;
 
 
 (** code and computation antiquotations **)
 
 local
 
 val mount_computationN = prefix_this "mount_computation";
 val mount_computation_convN = prefix_this "mount_computation_conv";
 val mount_computation_checkN = prefix_this "mount_computation_check";
 
 structure Code_Antiq_Data = Proof_Data
 (
   type T = { named_consts: string list,
     computation_Ts: typ list, computation_cTs: (string * typ) list,
     position_index: int,
     generated_code: (string * {
       name_for_tyco: string -> string,
       name_for_const: string -> string,
       of_term_for_typ: typ -> string
     }) lazy
   };
   val empty: T = { named_consts = [],
     computation_Ts = [], computation_cTs = [],
     position_index = 0,
     generated_code = Lazy.lazy (fn () => raise Fail "empty")
   };
   fun init _ = empty;
 );
 
 val current_position_index = #position_index o Code_Antiq_Data.get;
 
 fun register { named_consts, computation_Ts, computation_cTs } ctxt =
   let
     val data = Code_Antiq_Data.get ctxt;
     val named_consts' = union (op =) named_consts (#named_consts data);
     val computation_Ts' = union (op =) computation_Ts (#computation_Ts data);
     val computation_cTs' = union (op =) computation_cTs (#computation_cTs data);
     val position_index' = #position_index data + 1;
     fun generated_code' () =
       let
         val evals =
           Abs ("eval", map snd computation_cTs' ---> Term.aT [],
             list_comb (Bound 0, map Const computation_cTs'))
           |> preprocess_term { ctxt = ctxt } ctxt
       in Code_Thingol.dynamic_value ctxt
         (K I) (runtime_code ctxt NONE [] named_consts' computation_Ts') evals
       end;
   in
     ctxt
     |> Code_Antiq_Data.put { 
         named_consts = named_consts',
         computation_Ts = computation_Ts',
         computation_cTs = computation_cTs',
         position_index = position_index',
         generated_code = Lazy.lazy generated_code'
       }
   end;
 
 fun register_const const =
   register { named_consts = [const],
     computation_Ts = [],
     computation_cTs = [] };
 
 fun register_computation cTs T =
   register { named_consts = [],
     computation_Ts = [T],
     computation_cTs = cTs };
 
 fun print body_code_for ctxt ctxt' =
   let
     val position_index = current_position_index ctxt;
     val (code, name_ofs) = (Lazy.force o #generated_code o Code_Antiq_Data.get) ctxt';
     val context_code = if position_index = 0 then code else "";
     val body_code = body_code_for name_ofs (ML_Context.struct_name ctxt');
   in (context_code, body_code) end;
 
 fun print_code ctxt const =
   print (fn { name_for_const, ... } => fn prfx =>
     Long_Name.append prfx (name_for_const const)) ctxt;
 
 fun print_computation kind ctxt T =
   print (fn { of_term_for_typ, ... } => fn prfx =>
     enclose "(" ")" (space_implode " " [
       kind,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],
       (ML_Syntax.atomic o ML_Syntax.print_typ) T,
       Long_Name.append prfx (of_term_for_typ T)
     ])) ctxt;
 
 fun print_computation_check ctxt =
   print (fn { of_term_for_typ, ... } => fn prfx =>
     enclose "(" ")" (space_implode " " [
       mount_computation_checkN,
       "(Context.proof_of (Context.the_generic_context ()))",
       Long_Name.implode [prfx, generated_computationN, covered_constsN],
       Long_Name.append prfx (of_term_for_typ \<^typ>\<open>prop\<close>)
     ])) ctxt;
 
 fun add_all_constrs ctxt (dT as Type (tyco, Ts)) =
   case Code.get_type (Proof_Context.theory_of ctxt) tyco of
     ((vs, constrs), false) =>
       let
         val subst_TFree = the o AList.lookup (op =) (map fst vs ~~ Ts);
         val cs = map (fn (c, (_, Ts')) =>
           (c, (map o map_atyps) (fn TFree (v, _) => subst_TFree v) Ts'
             ---> dT)) constrs;
       in
         union (op =) cs
         #> fold (add_all_constrs ctxt) Ts
       end
   | (_, true) => I;
 
 fun prep_spec ctxt (raw_ts, raw_dTs) =
   let
     val ts = map (Syntax.check_term ctxt) raw_ts;
     val dTs = map (Syntax.check_typ ctxt) raw_dTs;
   in
     []
     |> (fold o fold_aterms)
       (fn (t as Const (cT as (_, T))) =>
         if not (monomorphic T) then error ("Polymorphic constant: " ^ Syntax.string_of_term ctxt t)
         else insert (op =) cT | _ => I) ts
     |> fold (fn dT =>
         if not (monomorphic dT) then error ("Polymorphic datatype: " ^ Syntax.string_of_typ ctxt dT)
         else add_all_constrs ctxt dT) dTs
   end;
 
 in
 
 fun ml_code_antiq raw_const ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val const = Code.check_const thy raw_const;
   in (print_code ctxt const, register_const const ctxt) end;
 
 fun gen_ml_computation_antiq kind (raw_T, raw_spec) ctxt =
   let
     val cTs = prep_spec ctxt raw_spec;
     val T = Syntax.check_typ ctxt raw_T;
     val _ = if not (monomorphic T)
       then error ("Polymorphic type: " ^ Syntax.string_of_typ ctxt T)
       else ();
   in (print_computation kind ctxt T, register_computation cTs T ctxt) end;
 
 val ml_computation_antiq = gen_ml_computation_antiq mount_computationN;
 
 val ml_computation_conv_antiq = gen_ml_computation_antiq mount_computation_convN;
 
 fun ml_computation_check_antiq raw_spec ctxt =
   let
     val cTs = insert (op =) (dest_Const \<^Const>\<open>holds\<close>) (prep_spec ctxt raw_spec);
   in (print_computation_check ctxt, register_computation cTs \<^typ>\<open>prop\<close> ctxt) end;
 
 end; (*local*)
 
 
 (** reflection support **)
 
 fun check_datatype thy tyco some_consts =
   let
     val declared_constrs = (map fst o snd o fst o Code.get_type thy) tyco;
     val constrs = case some_consts
      of SOME [] => []
       | SOME consts =>
           let
             val missing_constrs = subtract (op =) consts declared_constrs;
             val _ = if null missing_constrs then []
               else error ("Missing constructor(s) " ^ commas_quote missing_constrs
                 ^ " for datatype " ^ quote tyco);
             val false_constrs = subtract (op =) declared_constrs consts;
             val _ = if null false_constrs then []
               else error ("Non-constructor(s) " ^ commas_quote false_constrs
                 ^ " for datatype " ^ quote tyco)
           in consts end
       | NONE => declared_constrs;
   in (tyco, constrs) end;
 
 fun add_eval_tyco (tyco, tyco') thy =
   let
     val k = Sign.arity_number thy tyco;
     fun pr pr' _ [] = tyco'
       | pr pr' _ [ty] =
           Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
       | pr pr' _ tys =
           Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   in
     thy
     |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
   end;
 
 fun add_eval_constr (const, const') thy =
   let
     val k = Code.args_number thy const;
     fun pr pr' fxy ts = Code_Printer.brackify fxy
       (const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts)));
   in
     thy
     |> Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (k, pr)))]))
   end;
 
 fun add_eval_const (const, const') = Code_Target.set_printings (Constant
   (const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))]));
 
 fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
       thy
       |> Code_Target.add_reserved target module_name
       |> Context.theory_map (compile_ML true code)
       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
       |> fold (add_eval_const o apsnd Code_Printer.str) const_map
   | process_reflection (code, _) _ (SOME binding) thy =
       let
         val code_binding = Path.map_binding Code_Target.code_path binding;
         val preamble =
           "(* Generated from " ^
             Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
           "; DO NOT EDIT! *)";
-        val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy;
+        val thy' = Code_Target.export code_binding (Bytes.string (preamble ^ "\n\n" ^ code)) thy;
         val _ = Code_Target.code_export_message thy';
       in thy' end;
 
 fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name file_prefix thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val datatypes = map (fn (raw_tyco, raw_cos) =>
       (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
     val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
       |> apsnd flat;
     val functions = map (prep_const thy) raw_functions;
     val consts = constrs @ functions;
     val program = Code_Thingol.consts_program ctxt consts;
     val result = runtime_code'' ctxt module_name program tycos consts
       |> (apsnd o apsnd) (chop (length constrs));
   in
     thy
     |> process_reflection result module_name file_prefix
   end;
 
 val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
 val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const;
 
 
 (** Isar setup **)
 
 local
 
 val parse_consts_spec =
   Scan.optional (Scan.lift (Args.$$$ "terms" -- Args.colon) |-- Scan.repeat1 Args.term) []
   -- Scan.optional (Scan.lift (Args.$$$ "datatypes"  -- Args.colon) |-- Scan.repeat1 Args.typ) [];
 
 in
 
 val _ = Theory.setup
   (ML_Antiquotation.declaration \<^binding>\<open>code\<close>
     Args.term (K ml_code_antiq)
   #> ML_Antiquotation.declaration \<^binding>\<open>computation\<close>
     (Args.typ -- parse_consts_spec) (K ml_computation_antiq)
   #> ML_Antiquotation.declaration \<^binding>\<open>computation_conv\<close>
     (Args.typ -- parse_consts_spec) (K ml_computation_conv_antiq)
   #> ML_Antiquotation.declaration \<^binding>\<open>computation_check\<close>
     parse_consts_spec (K ml_computation_check_antiq));
 
 end;
 
 local
 
 val parse_datatype =
   Parse.name -- Scan.optional (\<^keyword>\<open>=\<close> |--
     (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
     || ((Parse.term ::: (Scan.repeat (\<^keyword>\<open>|\<close> |-- Parse.term))) >> SOME))) (SOME []);
 
 in
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_reflect\<close>
     "enrich runtime environment with generated code"
     (Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
       ::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
     -- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!!  (Scan.repeat1 Parse.name)) []
     -- Scan.option (\<^keyword>\<open>file_prefix\<close> |-- Parse.!!! (Parse.position Parse.embedded))
     >> (fn (((module_name, raw_datatypes), raw_functions), file_prefix) =>
       Toplevel.theory (fn thy =>
         code_reflect_cmd raw_datatypes raw_functions module_name
           (Option.map Path.explode_binding file_prefix) thy)));
 
 end; (*local*)
 
 
 (** using external SML files as substitute for proper definitions -- only for polyml!  **)
 
 local
 
 structure Loaded_Values = Theory_Data
 (
   type T = string list
   val empty = []
   fun merge data : T = Library.merge (op =) data
 );
 
 fun notify_val (string, value) = 
   let
     val _ = #enterVal ML_Env.name_space (string, value);
     val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   in () end;
 
 fun abort _ = error "Only value bindings allowed.";
 
 val notifying_context : ML_Compiler0.context =
  {name_space =
    {lookupVal    = #lookupVal ML_Env.name_space,
     lookupType   = #lookupType ML_Env.name_space,
     lookupFix    = #lookupFix ML_Env.name_space,
     lookupStruct = #lookupStruct ML_Env.name_space,
     lookupSig    = #lookupSig ML_Env.name_space,
     lookupFunct  = #lookupFunct ML_Env.name_space,
     enterVal     = notify_val,
     enterType    = abort,
     enterFix     = abort,
     enterStruct  = abort,
     enterSig     = abort,
     enterFunct   = abort,
     allVal       = #allVal ML_Env.name_space,
     allType      = #allType ML_Env.name_space,
     allFix       = #allFix ML_Env.name_space,
     allStruct    = #allStruct ML_Env.name_space,
     allSig       = #allSig ML_Env.name_space,
     allFunct     = #allFunct ML_Env.name_space},
   print_depth = NONE,
   here = #here ML_Env.context,
   print = #print ML_Env.context,
   error = #error ML_Env.context};
 
 in
 
 fun use_file filepath thy =
   let
     val thy' = Loaded_Values.put [] thy;
     val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
     val _ =
       ML_Compiler0.ML notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
         (File.read filepath);
     val thy'' = Context.the_global_context ();
     val names = Loaded_Values.get thy'';
   in (names, thy'') end;
 
 end;
 
 fun add_definiendum (ml_name, (b, T)) thy =
   thy
   |> Code_Target.add_reserved target ml_name
   |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
       [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
   #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
 
 fun process_file filepath (definienda, thy) =
   let
     val (ml_names, thy') = use_file filepath thy;
     val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
     val _ = if null superfluous then ()
       else error ("Value binding(s) " ^ commas_quote superfluous
         ^ " found in external file " ^ Path.print filepath
         ^ " not present among the given contants binding(s).");
     val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
     val thy'' = fold add_definiendum these_definienda thy';
     val definienda' = fold (AList.delete (op =)) ml_names definienda;
   in (definienda', thy'') end;
 
 fun polyml_as_definition bTs filepaths thy =
   let
     val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs;
     val (remaining, thy') = fold process_file filepaths (definienda, thy);
     val _ = if null remaining then ()
       else error ("Constant binding(s) " ^ commas_quote (map fst remaining)
         ^ " not present in external file(s).");
   in thy' end;
 
 end; (*struct*)
diff --git a/src/Tools/Code/code_target.ML b/src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML
+++ b/src/Tools/Code/code_target.ML
@@ -1,796 +1,798 @@
 (*  Title:      Tools/Code/code_target.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Generic infrastructure for target language data.
 *)
 
 signature CODE_TARGET =
 sig
   val cert_tyco: Proof.context -> string -> string
   val read_tyco: Proof.context -> string -> string
 
   datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
   val next_export: theory -> string * theory
 
   val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string
     -> int option -> Token.T list  -> Code_Thingol.program -> bool -> Code_Symbol.T list
     -> local_theory -> local_theory
   val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
-    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
+    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * Bytes.T) list * string option list
   val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
-    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
+    -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> Bytes.T
   val check_code_for: string -> bool -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
 
   val export_code: bool -> string list
     -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list
     -> local_theory -> local_theory
   val export_code_cmd: bool -> string list
     -> (((string * string) * ({physical: bool} * Input.source) option) * Token.T list) list
     -> local_theory -> local_theory
   val produce_code: Proof.context -> bool -> string list
-    -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
+    -> string -> string -> int option -> Token.T list -> (string list * Bytes.T) list * string option list
   val present_code: Proof.context -> string list -> Code_Symbol.T list
-    -> string -> string -> int option -> Token.T list -> string
+    -> string -> string -> int option -> Token.T list -> Bytes.T
   val check_code: bool -> string list -> ((string * bool) * Token.T list) list
     -> local_theory -> local_theory
 
   val codeN: string
   val generatedN: string
   val code_path: Path.T -> Path.T
   val code_export_message: theory -> unit
-  val export: Path.binding -> string -> theory -> theory
+  val export: Path.binding -> Bytes.T -> theory -> theory
   val compilation_text: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> (string list * string) list * string
+    -> (string list * Bytes.T) list * string
   val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
-    -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
+    -> ((string list * Bytes.T) list * string) * (Code_Symbol.T -> string option)
 
   type serializer
   type literals = Code_Printer.literals
   type language
   type ancestry
   val assert_target: theory -> string -> string
   val add_language: string * language -> theory -> theory
   val add_derived_target: string * ancestry -> theory -> theory
   val the_literals: Proof.context -> string -> literals
   val parse_args: 'a parser -> Token.T list -> 'a
   val default_code_width: int Config.T
 
   type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     -> theory -> theory
   val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, string * Code_Symbol.T list) symbol_attr_decl
     -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
 end;
 
 structure Code_Target : CODE_TARGET =
 struct
 
 open Basic_Code_Symbol;
 open Basic_Code_Thingol;
 
 type literals = Code_Printer.literals;
 type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl =
   (string * (string * 'a option) list, string * (string * 'b option) list,
     class * (string * 'c option) list, (class * class) * (string * 'd option) list,
     (class * string) * (string * 'e option) list,
     string * (string * 'f option) list) Code_Symbol.attr;
 
 type tyco_syntax = Code_Printer.tyco_syntax;
 type raw_const_syntax = Code_Printer.raw_const_syntax;
 
 
 (** checking and parsing of symbols **)
 
 fun cert_const ctxt const =
   let
     val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then ()
       else error ("No such constant: " ^ quote const);
   in const end;
 
 fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
 
 fun cert_tyco ctxt tyco =
   let
     val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
       else error ("No such type constructor: " ^ quote tyco);
   in tyco end;
 
 fun read_tyco ctxt =
   #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt;
 
 fun cert_class ctxt class =
   let
     val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
   in class end;
 
 val parse_classrel_ident = Parse.class --| \<^keyword>\<open><\<close> -- Parse.class;
 
 fun cert_inst ctxt (class, tyco) =
   (cert_class ctxt class, cert_tyco ctxt tyco);
 
 fun read_inst ctxt (raw_tyco, raw_class) =
   (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
 
 val parse_inst_ident = Parse.name --| \<^keyword>\<open>::\<close> -- Parse.class;
 
 fun cert_syms ctxt =
   Code_Symbol.map_attr (cert_const ctxt) (cert_tyco ctxt)
     (cert_class ctxt) (apply2 (cert_class ctxt)) (cert_inst ctxt) I;
 
 fun read_syms ctxt =
   Code_Symbol.map_attr (read_const ctxt) (read_tyco ctxt)
     (Proof_Context.read_class ctxt) (apply2 (Proof_Context.read_class ctxt)) (read_inst ctxt) I;
 
 fun cert_syms' ctxt =
   Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
     (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
 
 fun read_syms' ctxt =
   Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
     (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
 
 fun check_name is_module s =
   let
     val _ = if s = "" then error "Bad empty code name" else ();
     val xs = Long_Name.explode s;
     val xs' = if is_module
         then map (Name.desymbolize NONE) xs
       else if length xs < 2
         then error ("Bad code name without module component: " ^ quote s)
       else
         let
           val (ys, y) = split_last xs;
           val ys' = map (Name.desymbolize NONE) ys;
           val y' = Name.desymbolize NONE y;
         in ys' @ [y'] end;
   in if xs' = xs
     then if is_module then (xs, "") else split_last xs
     else error ("Invalid code name: " ^ quote s ^ "\n"
       ^ "better try " ^ quote (Long_Name.implode xs'))
   end;
 
 
 (** theory data **)
 
 datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
 
 type serializer = Token.T list
   -> Proof.context
   -> {
     reserved_syms: string list,
     identifiers: Code_Printer.identifiers,
     includes: (string * Pretty.T) list,
     class_syntax: string -> string option,
     tyco_syntax: string -> Code_Printer.tyco_syntax option,
     const_syntax: string -> Code_Printer.const_syntax option,
     module_name: string }
   -> Code_Thingol.program
   -> Code_Symbol.T list
   -> pretty_modules * (Code_Symbol.T -> string option);
 
 type language = {serializer: serializer, literals: literals,
   check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
   evaluation_args: Token.T list};
 
 type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
 
 val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
 
 type target = {serial: serial, language: language, ancestry: ancestry};
 
 structure Targets = Theory_Data
 (
   type T = (target * Code_Printer.data) Symtab.table * int;
   val empty = (Symtab.empty, 0);
   fun merge ((targets1, index1), (targets2, index2)) : T =
     let
       val targets' =
         Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
           if #serial target1 = #serial target2 then
           ({serial = #serial target1, language = #language target1,
             ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
             Code_Printer.merge_data (data1, data2))
           else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2)
       val index' = Int.max (index1, index2);
     in (targets', index') end;
 );
 
 val exists_target = Symtab.defined o #1 o Targets.get;
 val lookup_target_data = Symtab.lookup o #1 o Targets.get;
 fun assert_target thy target_name =
   if exists_target thy target_name
   then target_name
   else error ("Unknown code target language: " ^ quote target_name);
 
 fun reset_index thy =
   if #2 (Targets.get thy) = 0 then NONE
   else SOME ((Targets.map o apsnd) (K 0) thy);
 
 val _ = Theory.setup (Theory.at_begin reset_index);
 
 fun next_export thy =
   let
     val thy' = (Targets.map o apsnd) (fn i => i + 1) thy;
     val i = #2 (Targets.get thy');
   in ("export" ^ string_of_int i, thy') end;
 
 fun fold1 f xs = fold f (tl xs) (hd xs);
 
 fun join_ancestry thy target_name =
   let
     val _ = assert_target thy target_name;
     val the_target_data = the o lookup_target_data thy;
     val (target, this_data) = the_target_data target_name;
     val ancestry = #ancestry target;
     val modifies = rev (map snd ancestry);
     val modify = fold (curry (op o)) modifies I;
     val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
     val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
   in (modify, (target, data)) end;
 
 fun allocate_target target_name target thy =
   let
     val _ = if exists_target thy target_name
       then error ("Attempt to overwrite existing target " ^ quote target_name)
       else ();
   in
     thy
     |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))
   end;
 
 fun add_language (target_name, language) =
   allocate_target target_name {serial = serial (), language = language,
     ancestry = []};
 
 fun add_derived_target (target_name, initial_ancestry) thy =
   let
     val _ = if null initial_ancestry
       then error "Must derive from existing target(s)" else ();
     fun the_target_data target_name' = case lookup_target_data thy target_name' of
       NONE => error ("Unknown code target language: " ^ quote target_name')
     | SOME target_data' => target_data';
     val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
     val supremum = fold1 (fn target' => fn target =>
       if #serial target = #serial target'
       then target else error "Incompatible targets") targets;
     val ancestries = map #ancestry targets @ [initial_ancestry];
     val ancestry = fold1 (fn ancestry' => fn ancestry =>
       merge_ancestry (ancestry, ancestry')) ancestries;
   in
     allocate_target target_name {serial = #serial supremum, language = #language supremum,
       ancestry = ancestry} thy
   end;
 
 fun map_data target_name f thy =
   let
     val _ = assert_target thy target_name;
   in
     thy
     |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
   end;
 
 fun map_reserved target_name = map_data target_name o @{apply 3(1)};
 fun map_identifiers target_name = map_data target_name o @{apply 3(2)};
 fun map_printings target_name = map_data target_name o @{apply 3(3)};
 
 
 (** serializers **)
 
 val codeN = "code";
 val generatedN = "Generated_Code";
 
 val code_path = Path.append (Path.basic codeN);
 fun code_export_message thy = writeln (Export.message thy (Path.basic codeN));
 
 fun export binding content thy =
   let
     val thy' = thy |> Generated_Files.add_files (binding, content);
-    val _ = Export.export thy' binding [XML.Text content];
+    val _ = Export.export thy' binding (Bytes.contents_blob content);
   in thy' end;
 
 local
 
 fun export_logical (file_prefix, file_pos) format pretty_modules =
   let
     fun binding path = Path.binding (path, file_pos);
     val prefix = code_path file_prefix;
   in
     (case pretty_modules of
       Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p)
     | Hierarchy modules =>
         fold (fn (names, p) =>
           export (binding (prefix + Path.make names)) (format p)) modules)
     #> tap code_export_message
   end;
 
 fun export_physical root format pretty_modules =
   (case pretty_modules of
-    Singleton (_, p) => File.write root (format p)
+    Singleton (_, p) => Bytes.write root (format p)
   | Hierarchy code_modules =>
       (Isabelle_System.make_directory root;
         List.app (fn (names, p) =>
-          File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
+          Bytes.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
 
 in
 
 fun export_result some_file format (pretty_code, _) thy =
   (case some_file of
     NONE =>
       let val (file_prefix, thy') = next_export thy;
       in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end
   | SOME ({physical = false}, file_prefix) =>
       export_logical file_prefix format pretty_code thy
   | SOME ({physical = true}, (file, _)) =>
       let
         val root = File.full_path (Resources.master_directory thy) file;
         val _ = File.check_dir (Path.dir root);
         val _ = export_physical root format pretty_code;
       in thy end);
 
 fun produce_result syms width pretty_modules =
   let val format = Code_Printer.format [] width in
     (case pretty_modules of
       (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms)
     | (Hierarchy code_modules, deresolve) =>
         ((map o apsnd) format code_modules, map deresolve syms))
   end;
 
 fun present_result selects width (pretty_modules, _) =
   let val format = Code_Printer.format selects width in
     (case pretty_modules of
       Singleton (_, p) => format p
-    | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
+    | Hierarchy code_modules =>
+        Bytes.appends (separate (Bytes.string "\n\n") (map (format o #2) code_modules)))
   end;
 
 end;
 
 
 (** serializer usage **)
 
 (* technical aside: pretty printing width *)
 
 val default_code_width = Attrib.setup_config_int \<^binding>\<open>default_code_width\<close> (K 80);
 
 fun default_width ctxt = Config.get ctxt default_code_width;
 
 val the_width = the_default o default_width;
 
 
 (* montage *)
 
 fun the_language ctxt =
   #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt);
 
 fun the_literals ctxt = #literals o the_language ctxt;
 
 fun the_evaluation_args ctxt = #evaluation_args o the_language ctxt;
 
 local
 
 fun activate_target ctxt target_name =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (modify, (target, data)) = join_ancestry thy target_name;
     val serializer = (#serializer o #language) target;
   in { serializer = serializer, data = data, modify = modify } end;
 
 fun project_program_for_syms ctxt syms_hidden syms1 program1 =
   let
     val syms2 = subtract (op =) syms_hidden syms1;
     val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
     val unimplemented = Code_Thingol.unimplemented program2;
     val _ =
       if null unimplemented then ()
       else error ("No code equations for " ^
         commas (map (Proof_Context.markup_const ctxt) unimplemented));
     val syms3 = Code_Symbol.Graph.all_succs program2 syms2;
     val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
   in program3 end;
 
 fun project_includes_for_syms syms includes =
    let
      fun select_include (name, (content, cs)) =
        if null cs orelse exists (member (op =) syms) cs
        then SOME (name, content) else NONE;
   in map_filter select_include includes end;
 
 fun prepare_serializer ctxt target_name module_name args proto_program syms =
   let
     val { serializer, data, modify } = activate_target ctxt target_name;
     val printings = Code_Printer.the_printings data;
     val _ = if module_name = "" then () else (check_name true module_name; ())
     val hidden_syms = Code_Symbol.symbols_of printings;
     val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program;
     val prepared_syms = subtract (op =) hidden_syms syms;
     val all_syms = Code_Symbol.Graph.all_succs proto_program syms;
     val includes = project_includes_for_syms all_syms
       (Code_Symbol.dest_module_data printings);
     val prepared_serializer = serializer args ctxt {
       reserved_syms = Code_Printer.the_reserved data,
       identifiers = Code_Printer.the_identifiers data,
       includes = includes,
       const_syntax = Code_Symbol.lookup_constant_data printings,
       tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
       class_syntax = Code_Symbol.lookup_type_class_data printings,
       module_name = module_name };
   in
     (prepared_serializer o modify, (prepared_program, prepared_syms))
   end;
 
 fun invoke_serializer ctxt target_name module_name args program all_public syms =
   let
     val (prepared_serializer, (prepared_program, prepared_syms)) =
       prepare_serializer ctxt target_name module_name args program syms;
     val exports = if all_public then [] else prepared_syms;
   in
     Code_Preproc.timed_exec "serializing"
       (fn () => prepared_serializer prepared_program exports) ctxt
   end;
 
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
 
 in
 
 fun export_code_for some_file target_name module_name some_width args program all_public cs lthy =
   let
     val format = Code_Printer.format [] (the_width lthy some_width);
     val res = invoke_serializer lthy target_name module_name args program all_public cs;
   in Local_Theory.background_theory (export_result some_file format res) lthy end;
 
 fun produce_code_for ctxt target_name module_name some_width args =
   let
     val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   in fn program => fn all_public => fn syms =>
     produce_result syms (the_width ctxt some_width)
       (serializer program all_public syms)
   end;
 
 fun present_code_for ctxt target_name module_name some_width args =
   let
     val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
   in fn program => fn (syms, selects) =>
     present_result selects (the_width ctxt some_width) (serializer program false syms)
   end;
 
 fun check_code_for target_name strict args program all_public syms lthy =
   let
     val { env_var, make_destination, make_command } = #check (the_language lthy target_name);
     val format = Code_Printer.format [] 80;
     fun ext_check p =
       let
         val destination = make_destination p;
         val lthy' = lthy
           |> Local_Theory.background_theory
             (export_result (SOME ({physical = true}, (destination, Position.none))) format
               (invoke_serializer lthy target_name generatedN args program all_public syms));
         val cmd = make_command generatedN;
         val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
       in
         if Isabelle_System.bash context_cmd <> 0
         then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
         else lthy'
       end;
   in
     if not (env_var = "") andalso getenv env_var = "" then
       if strict
       then error (env_var ^ " not set; cannot check code for " ^ target_name)
       else (warning (env_var ^ " not set; skipped checking code for " ^ target_name); lthy)
     else Isabelle_System.with_tmp_dir "Code_Test" ext_check
   end;
 
 fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) =
   let
     val _ = if Code_Thingol.contains_dict_var t then
       error "Term to be evaluated contains free dictionaries" else ();
     val v' = singleton (Name.variant_list (map fst vs)) "a";
     val vs' = (v', []) :: vs;
     val ty' = ITyVar v' `-> ty;
     val program = prepared_program
       |> Code_Symbol.Graph.new_node (Code_Symbol.value,
           Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
       |> fold (curry (perhaps o try o
           Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
     val (pretty_code, deresolve) =
       prepared_serializer program (if all_public then [] else [Code_Symbol.value]);
     val (compilation_code, [SOME value_name]) =
       produce_result [Code_Symbol.value] width (pretty_code, deresolve);
   in ((compilation_code, value_name), deresolve) end;
 
 fun compilation_text' ctxt target_name some_module_name program syms =
   let
     val width = default_width ctxt;
     val evaluation_args = the_evaluation_args ctxt target_name;
     val (prepared_serializer, (prepared_program, _)) =
       prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms;
   in
     Code_Preproc.timed_exec "serializing"
       (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt
   end;
 
 fun compilation_text ctxt target_name program syms =
   fst oo compilation_text' ctxt target_name NONE program syms
 
 end; (* local *)
 
 
 (* code generation *)
 
 fun prep_destination (location, source) =
   let
     val s = Input.string_of source
     val pos = Input.pos_of source
     val delimited = Input.is_delimited source
   in
     if location = {physical = false}
     then (location, Path.explode_pos (s, pos))
     else
       let
         val _ =
           if s = ""
           then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument")
           else ();
         val _ =
           legacy_feature
             (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
               Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
         val _ = Position.report pos (Markup.language_path delimited);
         val path = #1 (Path.explode_pos (s, pos));
         val _ = Position.report pos (Markup.path (Path.implode_symbolic path));
       in (location, (path, pos)) end
   end;
 
 fun export_code all_public cs seris lthy =
   let
     val program = Code_Thingol.consts_program lthy cs;
   in
     (seris, lthy) |-> fold (fn (((target_name, module_name), some_file), args) =>
       export_code_for some_file target_name module_name NONE args
         program all_public (map Constant cs))
   end;
 
 fun export_code_cmd all_public raw_cs seris lthy =
   let
     val cs = Code_Thingol.read_const_exprs lthy raw_cs;
   in export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris) lthy end;
 
 fun produce_code ctxt all_public cs target_name some_width some_module_name args =
   let
     val program = Code_Thingol.consts_program ctxt cs;
   in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end;
 
 fun present_code ctxt cs syms target_name some_width some_module_name args =
   let
     val program = Code_Thingol.consts_program ctxt cs;
   in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
 
 fun check_code all_public cs seris lthy =
   let
     val program = Code_Thingol.consts_program lthy cs;
   in
     (seris, lthy) |-> fold (fn ((target_name, strict), args) =>
       check_code_for target_name strict args program all_public (map Constant cs))
   end;
 
 fun check_code_cmd all_public raw_cs seris lthy =
   check_code all_public (Code_Thingol.read_const_exprs lthy raw_cs) seris lthy;
 
 
 (** serializer configuration **)
 
 (* reserved symbol names *)
 
 fun add_reserved target_name sym thy =
   let
     val (_, (_, data)) = join_ancestry thy target_name;
     val _ = if member (op =) (Code_Printer.the_reserved data) sym
       then error ("Reserved symbol " ^ quote sym ^ " already declared")
       else ();
   in
     thy
     |> map_reserved target_name (insert (op =) sym)
   end;
 
 
 (* checking of syntax *)
 
 fun check_const_syntax ctxt target_name c syn =
   if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c
   then error ("Too many arguments in syntax for constant " ^ quote c)
   else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target_name) c syn;
 
 fun check_tyco_syntax ctxt target_name tyco syn =
   if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco
   then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
   else syn;
 
 
 (* custom symbol names *)
 
 fun arrange_name_decls x =
   let
     fun arrange is_module (sym, target_names) = map (fn (target, some_name) =>
       (target, (sym, Option.map (check_name is_module) some_name))) target_names;
   in
     Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false)
       (arrange false) (arrange false) (arrange true) x
   end;
 
 fun cert_name_decls ctxt = cert_syms' ctxt #> arrange_name_decls;
 
 fun read_name_decls ctxt = read_syms' ctxt #> arrange_name_decls;
 
 fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name);
 
 fun gen_set_identifiers prep_name_decl raw_name_decls thy =
   fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy;
 
 val set_identifiers = gen_set_identifiers cert_name_decls;
 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
 
 
 (* custom printings *)
 
 fun arrange_printings prep_syms ctxt =
   let
     fun arrange check (sym, target_syns) =
       map (fn (target_name, some_syn) =>
         (target_name, (sym, Option.map (check ctxt target_name sym) some_syn))) target_syns;
   in
     Code_Symbol.maps_attr'
       (arrange check_const_syntax) (arrange check_tyco_syntax)
         (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
         (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) =>
           (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
             map (prep_syms ctxt) raw_syms)))
   end;
 
 fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt;
 
 fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt;
 
 fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn);
 
 fun gen_set_printings prep_print_decl raw_print_decls thy =
   fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy;
 
 val set_printings = gen_set_printings cert_printings;
 val set_printings_cmd = gen_set_printings read_printings;
 
 
 (* concrete syntax *)
 
 fun parse_args f args =
   case Scan.read Token.stopper f args
    of SOME x => x
     | NONE => error "Bad serializer arguments";
 
 
 (** Isar setup **)
 
 val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
   (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
     \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
 
 local
 
 val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant;
 
 val parse_type_constructors = type_constructorK |-- Scan.repeat1 Parse.type_const >> map Type_Constructor;
 
 val parse_classes = type_classK |-- Scan.repeat1 Parse.class >> map Type_Class;
 
 val parse_class_relations = class_relationK |-- Scan.repeat1 parse_classrel_ident >> map Class_Relation;
 
 val parse_instances = class_instanceK |-- Scan.repeat1 parse_inst_ident >> map Class_Instance;
 
 val parse_simple_symbols = Scan.repeats1 (parse_constants || parse_type_constructors || parse_classes
   || parse_class_relations || parse_instances);
 
 fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
   parse_keyword |-- Parse.!!! (parse_isa --| (\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>)
     -- Parse.and_list1 (\<^keyword>\<open>(\<close> |-- (Parse.name --| \<^keyword>\<open>)\<close> -- Scan.option parse_target)));
 
 fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   parse_single_symbol_pragma constantK Parse.term parse_const
     >> Constant
   || parse_single_symbol_pragma type_constructorK Parse.type_const parse_tyco
     >> Type_Constructor
   || parse_single_symbol_pragma type_classK Parse.class parse_class
     >> Type_Class
   || parse_single_symbol_pragma class_relationK parse_classrel_ident parse_classrel
     >> Class_Relation
   || parse_single_symbol_pragma class_instanceK parse_inst_ident parse_inst
     >> Class_Instance
   || parse_single_symbol_pragma code_moduleK Parse.name parse_module
     >> Module;
 
 fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
   Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
     (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
 
 val code_expr_argsP = Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.args --| \<^keyword>\<open>)\<close>) [];
 
 fun code_expr_inP (all_public, raw_cs) =
   Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
     -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
     -- Scan.option
         ((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true})
           -- Parse.!!! Parse.path_input)
     -- code_expr_argsP))
       >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
 
 fun code_expr_checkingP (all_public, raw_cs) =
   (\<^keyword>\<open>checking\<close> |-- Parse.!!!
     (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\<open>?\<close> >> K false) true) -- code_expr_argsP)))
       >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
 
 in
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
     "declare words as reserved for target language"
     (Parse.name -- Scan.repeat1 Parse.name
       >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_identifier\<close> "declare mandatory names for code symbols"
     (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
       >> (Toplevel.theory o fold set_identifiers_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_printing\<close> "declare dedicated printing for code symbols"
     (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
       Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
       (Parse.embedded -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
       >> (Toplevel.theory o fold set_printings_cmd));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>export_code\<close> "generate executable code for constants"
     (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term
       :|-- (fn args => (code_expr_checkingP args || code_expr_inP args)));
 
 end;
 
 local
 
 val parse_const_terms = Args.theory -- Scan.repeat1 Args.term
   >> uncurry (fn thy => map (Code.check_const thy));
 
 fun parse_symbols keyword parse internalize mark_symbol =
   Scan.lift (keyword --| Args.colon) |-- Args.theory -- Scan.repeat1 parse
   >> uncurry (fn thy => map (mark_symbol o internalize thy));
 
 val parse_consts = parse_symbols constantK Args.term
   Code.check_const Constant;
 
 val parse_types = parse_symbols type_constructorK (Scan.lift Args.name)
   Sign.intern_type Type_Constructor;
 
 val parse_classes = parse_symbols type_classK (Scan.lift Args.name)
   Sign.intern_class Type_Class;
 
 val parse_instances = parse_symbols class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
   (fn thy => fn (raw_tyco, raw_class) =>
     (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) Class_Instance;
 
 in
 
 val _ = Theory.setup
   (Document_Output.antiquotation_raw \<^binding>\<open>code_stmts\<close>
     (parse_const_terms --
       Scan.repeats (parse_consts || parse_types || parse_classes || parse_instances)
       -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
     (fn ctxt => fn ((consts, symbols), (target_name, some_width)) =>
        present_code ctxt consts symbols
          target_name "Example" some_width []
+       |> Bytes.content
        |> trim_line
        |> Document_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));
 
 end;
 
 end; (*struct*)