# HG changeset patch
# User haftmann
# Date 1213988428 -7200
# Node ID 720c8115d7237b0aeabe25465d91a0a27da72203
# Parent  d6fef33c5c69b0f9f1f67f55a854bf5d93ccefa1
explicit thm context for error messages

diff -r d6fef33c5c69 -r 720c8115d723 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Fri Jun 20 21:00:27 2008 +0200
+++ b/src/Tools/code/code_target.ML	Fri Jun 20 21:00:28 2008 +0200
@@ -37,11 +37,11 @@
   val serialize: theory -> string -> string option -> Args.T list
     -> CodeThingol.program -> string list -> serialization;
   val compile: serialization -> unit;
-  val write: serialization -> unit;
+  val export: serialization -> unit;
   val file: Path.T -> serialization -> unit;
-  val string: serialization -> string;
+  val string: string list -> serialization -> string;
 
-  val code_of: theory -> string -> string -> string list -> string;
+  val code_of: theory -> string -> string -> string list -> string list -> string;
   val eval_conv: string * (unit -> thm) option ref
     -> theory -> cterm -> string list -> thm;
   val eval_term: string * (unit -> 'a) option ref
@@ -70,7 +70,7 @@
 fun enum_default default sep opn cls [] = str default
   | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
 
-datatype destination = Compile | Write | File of Path.T | String;
+datatype destination = Compile | Export | File of Path.T | String of string list;
 type serialization = destination -> string option;
 
 val code_width = ref 80; (*FIXME after Pretty module no longer depends on print mode*)
@@ -80,9 +80,12 @@
 
 (*FIXME why another code_setmp?*)
 fun compile f = (code_setmp f Compile; ());
-fun write f = (code_setmp f Write; ());
+fun export f = (code_setmp f Export; ());
 fun file p f = (code_setmp f (File p); ());
-fun string f = the (code_setmp f String);
+fun string cs f = the (code_setmp f (String cs));
+
+fun stmt_names_of_destination (String stmts) = stmts
+  | stmt_names_of_destination _ = [];
 
 
 (** generic syntax **)
@@ -124,7 +127,7 @@
 type typ_syntax = int * ((fixity -> itype -> Pretty.T)
   -> fixity -> itype list -> Pretty.T);
 type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
-  -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+  -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
 
 
 (** theory data **)
@@ -153,7 +156,7 @@
        Symtab.join (K snd) (const1, const2))
   );
 
-type serializer = (*FIXME order of arguments*)
+type serializer =
   string option                         (*module name*)
   -> Args.T list                        (*arguments*)
   -> (string -> string)                 (*labelled_name*)
@@ -297,6 +300,8 @@
 
 (* list, char, string, numeral and monad abstract syntax transformations *)
 
+fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
+
 fun implode_list c_nil c_cons t =
   let
     fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
@@ -330,20 +335,20 @@
     else NONE
   end;
 
-fun implode_numeral negative c_pls c_min c_bit0 c_bit1 =
+fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
   let
     fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
           else if c = c_bit1 then 1
-          else error "Illegal numeral expression: illegal bit"
-      | dest_bit _ = error "Illegal numeral expression: illegal bit";
+          else nerror thm "Illegal numeral expression: illegal bit"
+      | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
     fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
           else if c = c_min then
             if negative then SOME ~1 else NONE
-          else error "Illegal numeral expression: illegal leading digit"
+          else nerror thm "Illegal numeral expression: illegal leading digit"
       | dest_numeral (t1 `$ t2) =
           let val (n, b) = (dest_numeral t2, dest_bit t1)
           in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
-      | dest_numeral _ = error "Illegal numeral expression: illegal term";
+      | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
   in dest_numeral #> the_default 0 end;
 
 fun implode_monad c_bind t =
@@ -364,25 +369,25 @@
 
 (* applications and bindings *)
 
-fun gen_pr_app pr_app pr_term syntax_const labelled_name is_cons
-      lhs vars fxy (app as ((c, (_, tys)), ts)) =
+fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
+    vars fxy (app as ((c, (_, tys)), ts)) =
   case syntax_const c
-   of NONE => if lhs andalso not (is_cons c) then
-          error ("Non-constructor on left hand side of equation: " ^ labelled_name c)
-        else brackify fxy (pr_app lhs vars app)
+   of NONE => if pat andalso not (is_cons c) then
+        nerror thm "Non-constructor in pattern "
+        else brackify fxy (pr_app thm pat vars app)
     | SOME (i, pr) =>
         let
           val k = if i < 0 then length tys else i;
-          fun pr' fxy ts = pr (pr_term lhs) vars fxy (ts ~~ curry Library.take k tys);
+          fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
         in if k = length ts
           then pr' fxy ts
         else if k < length ts
           then case chop k ts of (ts1, ts2) =>
-            brackify fxy (pr' APP ts1 :: map (pr_term lhs vars BR) ts2)
-          else pr_term lhs vars fxy (CodeThingol.eta_expand app k)
+            brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
+          else pr_term thm pat vars fxy (CodeThingol.eta_expand app k)
         end;
 
-fun gen_pr_bind pr_bind pr_term (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
   let
     val vs = case pat
      of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
@@ -390,7 +395,7 @@
     val vars' = CodeName.intro_vars (the_list v) vars;
     val vars'' = CodeName.intro_vars vs vars';
     val v' = Option.map (CodeName.lookup_var vars') v;
-    val pat' = Option.map (pr_term true vars'' fxy) pat;
+    val pat' = Option.map (pr_term thm true vars'' fxy) pat;
   in (pr_bind ((v', pat'), ty), vars'') end;
 
 
@@ -425,12 +430,17 @@
 (** SML/OCaml serializer **)
 
 datatype ml_stmt =
-    MLFuns of (string * (typscheme * (iterm list * iterm) list)) list
+    MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
   | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
   | MLClass of string * (vname * ((class * string) list * (string * itype) list))
   | MLClassinst of string * ((class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
-      * (string * const) list));
+      * ((string * const) * thm) list));
+
+fun stmt_names_of (MLFuns fs) = map fst fs
+  | stmt_names_of (MLDatas ds) = map fst ds
+  | stmt_names_of (MLClass (c, _)) = [c]
+  | stmt_names_of (MLClassinst (i, _)) = [i];
 
 fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
   let
@@ -469,94 +479,86 @@
         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
       end
-    and pr_typ fxy (tyco `%% tys) =
-          (case syntax_tyco tyco
-           of NONE => pr_tycoexpr fxy (tyco, tys)
-            | SOME (i, pr) =>
-                if not (i = length tys)
-                then error ("Number of argument mismatch in customary serialization: "
-                  ^ (string_of_int o length) tys ^ " given, "
-                  ^ string_of_int i ^ " expected")
-                else pr pr_typ fxy tys)
-      | pr_typ fxy (ITyVar v) =
-          str ("'" ^ v);
-    fun pr_term lhs vars fxy (IConst c) =
-          pr_app lhs vars fxy (c, [])
-      | pr_term lhs vars fxy (IVar v) =
+    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+         of NONE => pr_tycoexpr fxy (tyco, tys)
+          | SOME (i, pr) => pr pr_typ fxy tys)
+      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
+    fun pr_term thm pat vars fxy (IConst c) =
+          pr_app thm pat vars fxy (c, [])
+      | pr_term thm pat vars fxy (IVar v) =
           str (CodeName.lookup_var vars v)
-      | pr_term lhs vars fxy (t as t1 `$ t2) =
+      | pr_term thm pat vars fxy (t as t1 `$ t2) =
           (case CodeThingol.unfold_const_app t
-           of SOME c_ts => pr_app lhs vars fxy c_ts
+           of SOME c_ts => pr_app thm pat vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
-      | pr_term lhs vars fxy (t as _ `|-> _) =
+                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
+      | pr_term thm pat vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodeThingol.unfold_abs t;
             fun pr ((v, pat), ty) =
-              pr_bind NOBR ((SOME v, pat), ty)
+              pr_bind thm NOBR ((SOME v, pat), ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (ps @ [pr_term lhs vars' NOBR t']) end
-      | pr_term lhs vars fxy (ICase (cases as (_, t0))) =
+          in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
+      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
           (case CodeThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then pr_case vars fxy cases
-                else pr_app lhs vars fxy c_ts
-            | NONE => pr_case vars fxy cases)
-    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
+                then pr_case thm vars fxy cases
+                else pr_app thm pat vars fxy c_ts
+            | NONE => pr_case thm vars fxy cases)
+    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then let
         val k = length tys
       in if k < 2 then 
-        (str o deresolve) c :: map (pr_term lhs vars BR) ts
+        (str o deresolve) c :: map (pr_term thm pat vars BR) ts
       else if k = length ts then
-        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term lhs vars NOBR) ts)]
-      else [pr_term lhs vars BR (CodeThingol.eta_expand app k)] end else
+        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
+      else [pr_term thm pat vars BR (CodeThingol.eta_expand app k)] end else
         (str o deresolve) c
-          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts
-    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
-      labelled_name is_cons lhs vars
+          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
+    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
-    and pr_case vars fxy (cases as ((_, [_]), _)) =
+    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
+    and pr_case thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind NOBR ((NONE, SOME pat), ty)
-              |>> (fn p => semicolon [str "val", p, str "=", pr_term false vars NOBR t])
+              |> pr_bind thm NOBR ((NONE, SOME pat), ty)
+              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
             Pretty.chunks [
               [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
-              [str ("in"), Pretty.fbrk, pr_term false vars' NOBR t'] |> Pretty.block,
+              [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
               str ("end")
             ]
           end
-      | pr_case vars fxy (((td, ty), b::bs), _) =
+      | pr_case thm vars fxy (((td, ty), b::bs), _) =
           let
             fun pr delim (pat, t) =
               let
-                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
               in
-                concat [str delim, p, str "=>", pr_term false vars' NOBR t]
+                concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
               end;
           in
             (Pretty.enclose "(" ")" o single o brackify fxy) (
               str "case"
-              :: pr_term false vars NOBR td
+              :: pr_term thm false vars NOBR td
               :: pr "of" b
               :: map (pr "|") bs
             )
           end
-      | pr_case vars fxy ((_, []), _) = str "raise Fail \"empty case\""
+      | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
     fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
           let
             val definer =
               let
-                fun no_args _ ((ts, _) :: _) = length ts
+                fun no_args _ (((ts, _), _) :: _) = length ts
                   | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
                 fun mk 0 [] = "val"
                   | mk 0 vs = if (null o filter_out (null o snd)) vs
@@ -590,7 +592,7 @@
                     val vs_dict = filter_out (null o snd) vs;
                     val shift = if null eqs' then I else
                       map (Pretty.block o single o Pretty.block o single);
-                    fun pr_eq definer (ts, t) =
+                    fun pr_eq definer ((ts, t), thm) =
                       let
                         val consts = map_filter
                           (fn c => if (is_some o syntax_const) c
@@ -607,8 +609,8 @@
                              then [str ":", pr_typ NOBR ty]
                              else
                                pr_tyvar_dicts vs_dict
-                               @ map (pr_term true vars BR) ts)
-                       @ [str "=", pr_term false vars NOBR t]
+                               @ map (pr_term thm true vars BR) ts)
+                       @ [str "=", pr_term thm false vars NOBR t]
                         )
                       end
                   in
@@ -697,11 +699,11 @@
                 str "=",
                 pr_dicts NOBR [DictConst dss]
               ];
-            fun pr_classparam (classparam, c_inst) =
+            fun pr_classparam ((classparam, c_inst), thm) =
               concat [
                 (str o pr_label_classparam) classparam,
                 str "=",
-                pr_app false reserved_names NOBR (c_inst, [])
+                pr_app thm false reserved_names NOBR (c_inst, [])
               ];
           in
             semicolon ([
@@ -757,80 +759,72 @@
         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
       end
-    and pr_typ fxy (tyco `%% tys) =
-          (case syntax_tyco tyco
-           of NONE => pr_tycoexpr fxy (tyco, tys)
-            | SOME (i, pr) =>
-                if not (i = length tys)
-                then error ("Number of argument mismatch in customary serialization: "
-                  ^ (string_of_int o length) tys ^ " given, "
-                  ^ string_of_int i ^ " expected")
-                else pr pr_typ fxy tys)
-      | pr_typ fxy (ITyVar v) =
-          str ("'" ^ v);
-    fun pr_term lhs vars fxy (IConst c) =
-          pr_app lhs vars fxy (c, [])
-      | pr_term lhs vars fxy (IVar v) =
+    and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+         of NONE => pr_tycoexpr fxy (tyco, tys)
+          | SOME (i, pr) => pr pr_typ fxy tys)
+      | pr_typ fxy (ITyVar v) = str ("'" ^ v);
+    fun pr_term thm pat vars fxy (IConst c) =
+          pr_app thm pat vars fxy (c, [])
+      | pr_term thm pat vars fxy (IVar v) =
           str (CodeName.lookup_var vars v)
-      | pr_term lhs vars fxy (t as t1 `$ t2) =
+      | pr_term thm pat vars fxy (t as t1 `$ t2) =
           (case CodeThingol.unfold_const_app t
-           of SOME c_ts => pr_app lhs vars fxy c_ts
+           of SOME c_ts => pr_app thm pat vars fxy c_ts
             | NONE =>
-                brackify fxy [pr_term lhs vars NOBR t1, pr_term lhs vars BR t2])
-      | pr_term lhs vars fxy (t as _ `|-> _) =
+                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
+      | pr_term thm pat vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodeThingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind BR ((SOME v, pat), ty);
+            fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (str "fun" :: ps @ str "->" @@ pr_term lhs vars' NOBR t') end
-      | pr_term lhs vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
+          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
+      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then pr_case vars fxy cases
-                else pr_app lhs vars fxy c_ts
-            | NONE => pr_case vars fxy cases)
-    and pr_app' lhs vars (app as ((c, (iss, tys)), ts)) =
+                then pr_case thm vars fxy cases
+                else pr_app thm pat vars fxy c_ts
+            | NONE => pr_case thm vars fxy cases)
+    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
       if is_cons c then
         if length tys = length ts
         then case ts
          of [] => [(str o deresolve) c]
-          | [t] => [(str o deresolve) c, pr_term lhs vars BR t]
+          | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
           | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
-                    (map (pr_term lhs vars NOBR) ts)]
-        else [pr_term lhs vars BR (CodeThingol.eta_expand app (length tys))]
+                    (map (pr_term thm pat vars NOBR) ts)]
+        else [pr_term thm pat vars BR (CodeThingol.eta_expand app (length tys))]
       else (str o deresolve) c
-        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term lhs vars BR) ts)
-    and pr_app lhs vars = gen_pr_app pr_app' pr_term syntax_const
-      labelled_name is_cons lhs vars
+        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
+    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
     and pr_bind' ((NONE, NONE), _) = str "_"
       | pr_bind' ((SOME v, NONE), _) = str v
       | pr_bind' ((NONE, SOME p), _) = p
       | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
-    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
-    and pr_case vars fxy (cases as ((_, [_]), _)) =
+    and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
+    and pr_case thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind NOBR ((NONE, SOME pat), ty)
+              |> pr_bind thm NOBR ((NONE, SOME pat), ty)
               |>> (fn p => concat
-                  [str "let", p, str "=", pr_term false vars NOBR t, str "in"])
+                  [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
-          in Pretty.chunks (ps @| pr_term false vars' NOBR t') end
-      | pr_case vars fxy (((td, ty), b::bs), _) =
+          in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
+      | pr_case thm vars fxy (((td, ty), b::bs), _) =
           let
             fun pr delim (pat, t) =
               let
-                val (p, vars') = pr_bind NOBR ((NONE, SOME pat), ty) vars;
-              in concat [str delim, p, str "->", pr_term false vars' NOBR t] end;
+                val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
+              in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
           in
             (Pretty.enclose "(" ")" o single o brackify fxy) (
               str "match"
-              :: pr_term false vars NOBR td
+              :: pr_term thm false vars NOBR td
               :: pr "with" b
               :: map (pr "|") bs
             )
           end
-      | pr_case vars fxy ((_, []), _) = str "failwith \"empty case\"";
+      | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
     fun fish_params vars eqs =
       let
         fun fish_param _ (w as SOME _) = w
@@ -846,7 +840,7 @@
       in map (CodeName.lookup_var vars') fished3 end;
     fun pr_stmt (MLFuns (funns as funn :: funns')) =
           let
-            fun pr_eq (ts, t) =
+            fun pr_eq ((ts, t), thm) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
@@ -857,9 +851,9 @@
                   |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in concat [
-                (Pretty.block o Pretty.commas) (map (pr_term true vars NOBR) ts),
+                (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
                 str "->",
-                pr_term false vars NOBR t
+                pr_term thm false vars NOBR t
               ] end;
             fun pr_eqs name ty [] =
                   let
@@ -874,7 +868,7 @@
                       @@ str exc_str
                     )
                   end
-              | pr_eqs _ _ [(ts, t)] =
+              | pr_eqs _ _ [((ts, t), thm)] =
                   let
                     val consts = map_filter
                       (fn c => if (is_some o syntax_const) c
@@ -886,12 +880,12 @@
                           (insert (op =)) ts []);
                   in
                     concat (
-                      map (pr_term true vars BR) ts
+                      map (pr_term thm true vars BR) ts
                       @ str "="
-                      @@ pr_term false vars NOBR t
+                      @@ pr_term thm false vars NOBR t
                     )
                   end
-              | pr_eqs _ _ (eqs as (eq as ([_], _)) :: eqs') =
+              | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
                   Pretty.block (
                     str "="
                     :: Pretty.brk 1
@@ -907,10 +901,10 @@
                       (fn c => if (is_some o syntax_const) c
                         then NONE else (SOME o NameSpace.base o deresolve) c)
                         ((fold o CodeThingol.fold_constnames)
-                          (insert (op =)) (map snd eqs) []);
+                          (insert (op =)) (map (snd o fst) eqs) []);
                     val vars = reserved_names
                       |> CodeName.intro_vars consts;
-                    val dummy_parms = (map str o fish_params vars o map fst) eqs;
+                    val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
@@ -1004,11 +998,11 @@
                 str "=",
                 pr_dicts NOBR [DictConst dss]
               ];
-            fun pr_classparam_inst (classparam, c_inst) =
+            fun pr_classparam_inst ((classparam, c_inst), thm) =
               concat [
                 (str o deresolve) classparam,
                 str "=",
-                pr_app false reserved_names NOBR (c_inst, [])
+                pr_app thm false reserved_names NOBR (c_inst, [])
               ];
           in
             concat (
@@ -1088,7 +1082,7 @@
       fold_map
         (fn (name, CodeThingol.Fun stmt) =>
               map_nsp_fun_yield (mk_name_stmt false name) #>>
-                rpair (name, (apsnd o map) fst stmt)
+                rpair (name, stmt)
           | (name, _) =>
               error ("Function block containing illegal statement: " ^ labelled_name name)
         ) stmts
@@ -1123,7 +1117,7 @@
              | [stmt] => MLClass stmt)));
     fun add_inst [(name, CodeThingol.Classinst stmt)] =
       map_nsp_fun_yield (mk_name_stmt false name)
-      #>> (fn base => ([base], MLClassinst (name, (apsnd o apsnd o map) fst stmt)));
+      #>> (fn base => ([base], MLClassinst (name, stmt)));
     fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
           add_funs stmts
       | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
@@ -1200,31 +1194,38 @@
         error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, nodes) end;
 
-fun serialize_ml compile pr_module pr_stmt projection module_name labelled_name reserved_names includes raw_module_alias
+fun serialize_ml compile pr_module pr_stmt projection raw_module_name labelled_name reserved_names includes raw_module_alias
   _ syntax_tyco syntax_const program cs destination =
   let
     val is_cons = CodeThingol.is_cons program;
+    val stmt_names = stmt_names_of_destination destination;
+    val module_name = if null stmt_names then raw_module_name else SOME "Code";
     val (deresolver, nodes) = ml_node_of_program labelled_name module_name
       reserved_names raw_module_alias program;
     val reserved_names = CodeName.make_vars reserved_names;
     fun pr_node prefix (Dummy _) =
           NONE
-      | pr_node prefix (Stmt (_, def)) =
-          SOME (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
-            (deresolver prefix) is_cons def)
+      | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
+          (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
+            (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
+              (deresolver prefix) is_cons stmt)
+          else NONE
       | pr_node prefix (Module (module_name, (_, nodes))) =
-          SOME (pr_module module_name (
-            separate (str "")
-                ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
-                o rev o flat o Graph.strong_conn) nodes)));
+          let
+            val ps = separate (str "")
+              ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
+                o rev o flat o Graph.strong_conn) nodes)
+          in SOME (case destination of String _ => Pretty.chunks ps
+           | _ => pr_module module_name ps)
+          end;
     val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
       cs;
     val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
       (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
     fun output Compile = K NONE o compile o code_of_pretty
-      | output Write = K NONE o code_writeln
+      | output Export = K NONE o code_writeln
       | output (File file) = K NONE o File.write file o code_of_pretty
-      | output String = SOME o code_of_pretty;
+      | output (String _) = SOME o code_of_pretty;
   in projection (output destination p) cs' end;
 
 end; (*local*)
@@ -1242,13 +1243,13 @@
 
 (** Haskell serializer **)
 
-val pr_haskell_bind =
+fun pr_haskell_bind pr_term =
   let
     fun pr_bind ((NONE, NONE), _) = str "_"
       | pr_bind ((SOME v, NONE), _) = str v
       | pr_bind ((NONE, SOME p), _) = p
       | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
-  in gen_pr_bind pr_bind end;
+  in gen_pr_bind pr_bind pr_term end;
 
 fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
     init_syms deresolve is_cons contr_classparam_typs deriving_show =
@@ -1274,90 +1275,81 @@
           (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
     fun pr_tycoexpr tyvars fxy (tyco, tys) =
       brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
-    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) =
-          (case syntax_tyco tyco
-           of NONE =>
-                pr_tycoexpr tyvars fxy (deresolve tyco, tys)
-            | SOME (i, pr) =>
-                if not (i = length tys)
-                then error ("Number of argument mismatch in customary serialization: "
-                  ^ (string_of_int o length) tys ^ " given, "
-                  ^ string_of_int i ^ " expected")
-                else pr (pr_typ tyvars) fxy tys)
-      | pr_typ tyvars fxy (ITyVar v) =
-          (str o CodeName.lookup_var tyvars) v;
+    and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+         of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
+          | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
+      | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
     fun pr_typdecl tyvars (vs, tycoexpr) =
       Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
     fun pr_typscheme tyvars (vs, ty) =
       Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
-    fun pr_term tyvars lhs vars fxy (IConst c) =
-          pr_app tyvars lhs vars fxy (c, [])
-      | pr_term tyvars lhs vars fxy (t as (t1 `$ t2)) =
+    fun pr_term tyvars thm pat vars fxy (IConst c) =
+          pr_app tyvars thm pat vars fxy (c, [])
+      | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
           (case CodeThingol.unfold_const_app t
-           of SOME app => pr_app tyvars lhs vars fxy app
+           of SOME app => pr_app tyvars thm pat vars fxy app
             | _ =>
                 brackify fxy [
-                  pr_term tyvars lhs vars NOBR t1,
-                  pr_term tyvars lhs vars BR t2
+                  pr_term tyvars thm pat vars NOBR t1,
+                  pr_term tyvars thm pat vars BR t2
                 ])
-      | pr_term tyvars lhs vars fxy (IVar v) =
+      | pr_term tyvars thm pat vars fxy (IVar v) =
           (str o CodeName.lookup_var vars) v
-      | pr_term tyvars lhs vars fxy (t as _ `|-> _) =
+      | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
           let
             val (binds, t') = CodeThingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind tyvars BR ((SOME v, pat), ty);
+            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
             val (ps, vars') = fold_map pr binds vars;
-          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars lhs vars' NOBR t') end
-      | pr_term tyvars lhs vars fxy (ICase (cases as (_, t0))) =
+          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
+      | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
           (case CodeThingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
-                then pr_case tyvars vars fxy cases
-                else pr_app tyvars lhs vars fxy c_ts
-            | NONE => pr_case tyvars vars fxy cases)
-    and pr_app' tyvars lhs vars ((c, (_, tys)), ts) = case contr_classparam_typs c
-     of [] => (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
+                then pr_case tyvars thm vars fxy cases
+                else pr_app tyvars thm pat vars fxy c_ts
+            | NONE => pr_case tyvars thm vars fxy cases)
+    and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+     of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
       | fingerprint => let
           val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
           val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
             (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
-          fun pr_term_anno (t, NONE) _ = pr_term tyvars lhs vars BR t
+          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
             | pr_term_anno (t, SOME _) ty =
-                brackets [pr_term tyvars lhs vars NOBR t, str "::", pr_typ tyvars NOBR ty];
+                brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
         in
           if needs_annotation then
             (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
-          else (str o deresolve) c :: map (pr_term tyvars lhs vars BR) ts
+          else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
         end
-    and pr_app tyvars lhs vars  = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
-      labelled_name is_cons lhs vars
+    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
     and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
-    and pr_case tyvars vars fxy (cases as ((_, [_]), _)) =
+    and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t) = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind tyvars BR ((NONE, SOME pat), ty)
-              |>> (fn p => semicolon [p, str "=", pr_term tyvars false vars NOBR t])
+              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
             Pretty.block_enclose (
               str "let {",
-              concat [str "}", str "in", pr_term tyvars false vars' NOBR t]
+              concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
             ) ps
           end
-      | pr_case tyvars vars fxy (((td, ty), bs as _ :: _), _) =
+      | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
           let
             fun pr (pat, t) =
               let
-                val (p, vars') = pr_bind tyvars NOBR ((NONE, SOME pat), ty) vars;
-              in semicolon [p, str "->", pr_term tyvars false vars' NOBR t] end;
+                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+              in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
           in
             Pretty.block_enclose (
-              concat [str "(case", pr_term tyvars false vars NOBR td, str "of", str "{"],
+              concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
               str "})"
             ) (map pr bs)
           end
-      | pr_case tyvars vars fxy ((_, []), _) = str "error \"empty case\"";
+      | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
     fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
           let
             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
@@ -1383,7 +1375,7 @@
       | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
           let
             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
-            fun pr_eq ((ts, t), _) =
+            fun pr_eq ((ts, t), thm) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
@@ -1396,9 +1388,9 @@
               in
                 semicolon (
                   (str o deresolve_base) name
-                  :: map (pr_term tyvars true vars BR) ts
+                  :: map (pr_term tyvars thm true vars BR) ts
                   @ str "="
-                  @@ pr_term tyvars false vars NOBR t
+                  @@ pr_term tyvars thm false vars NOBR t
                 )
               end;
           in
@@ -1475,11 +1467,11 @@
       | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
             val tyvars = CodeName.intro_vars (map fst vs) init_syms;
-            fun pr_instdef ((classparam, c_inst), _) =
+            fun pr_instdef ((classparam, c_inst), thm) =
               semicolon [
                 (str o classparam_name class) classparam,
                 str "=",
-                pr_app tyvars false init_syms NOBR (c_inst, [])
+                pr_app tyvars thm false init_syms NOBR (c_inst, [])
               ];
           in
             Pretty.block_enclose (
@@ -1497,9 +1489,9 @@
 
 fun pretty_haskell_monad c_bind =
   let
-    fun pretty pr vars fxy [(t, _)] =
+    fun pretty pr thm pat vars fxy [(t, _)] =
       let
-        val pr_bind = pr_haskell_bind (K pr);
+        val pr_bind = pr_haskell_bind (K (K pr)) thm;
         fun pr_monad (NONE, t) vars =
               (semicolon [pr vars NOBR t], vars)
           | pr_monad (SOME (bind, true), t) vars = vars
@@ -1565,10 +1557,12 @@
         handle Option => error ("Unknown statement name: " ^ labelled_name name);
   in (deresolver, hs_program) end;
 
-fun serialize_haskell module_prefix module_name string_classes labelled_name
+fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
     reserved_names includes raw_module_alias
     syntax_class syntax_tyco syntax_const program cs destination =
   let
+    val stmt_names = stmt_names_of_destination destination;
+    val module_name = if null stmt_names then raw_module_name else SOME "Code";
     val (deresolver, hs_program) = haskell_program_of_program labelled_name
       module_name module_prefix reserved_names raw_module_alias program;
     val is_cons = CodeThingol.is_cons program;
@@ -1599,7 +1593,7 @@
         str "",
         str "}"
       ]);
-    fun serialize_module (module_name', (deps, (stmts, _))) =
+    fun serialize_module1 (module_name', (deps, (stmts, _))) =
       let
         val stmt_names = map fst stmts;
         val deps' = subtract (op =) stmt_names deps
@@ -1625,6 +1619,15 @@
                 | (_, (_, NONE)) => NONE) stmts)
           )
       in pr_module module_name' content end;
+    fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
+      separate (str "") (map_filter
+        (fn (name, (_, SOME stmt)) => if null stmt_names
+              orelse member (op =) stmt_names name
+              then SOME (pr_stmt false (name, stmt))
+              else NONE
+          | (_, (_, NONE)) => NONE) stmts));
+    val serialize_module = case destination of String _ => pair "" o serialize_module2
+      | _ => serialize_module1;
     fun write_module destination (modlname, content) =
       let
         val filename = case modlname
@@ -1635,9 +1638,9 @@
         val _ = File.mkdir (Path.dir pathname);
       in File.write pathname (code_of_pretty content) end
     fun output Compile = error ("Haskell: no internal compilation")
-      | output Write = K NONE o map (code_writeln o snd)
+      | output Export = K NONE o map (code_writeln o snd)
       | output (File destination) = K NONE o map (write_module destination)
-      | output String = SOME o cat_lines o map (code_of_pretty o snd);
+      | output (String _) = SOME o cat_lines o map (code_of_pretty o snd);
   in
     output destination (map (uncurry pr_module) includes
       @ map serialize_module (Symtab.dest hs_program))
@@ -1723,7 +1726,7 @@
   let
     val pretty_ops = pr_pretty target;
     val mk_list = #pretty_list pretty_ops;
-    fun pretty pr vars fxy [(t1, _), (t2, _)] =
+    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (implode_list c_nil c_cons t2)
        of SOME ts => mk_list (map (pr vars NOBR) ts)
         | NONE => default_list (#infix_cons pretty_ops) (pr vars) fxy t1 t2;
@@ -1735,7 +1738,7 @@
     val mk_list = #pretty_list pretty_ops;
     val mk_char = #pretty_char pretty_ops;
     val mk_string = #pretty_string pretty_ops;
-    fun pretty pr vars fxy [(t1, _), (t2, _)] =
+    fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
       case Option.map (cons t1) (implode_list c_nil c_cons t2)
        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
            of SOME p => p
@@ -1746,17 +1749,17 @@
 fun pretty_char c_char c_nibbles target =
   let
     val mk_char = #pretty_char (pr_pretty target);
-    fun pretty _ _ _ [(t1, _), (t2, _)] =
+    fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
       case decode_char c_nibbles (t1, t2)
        of SOME c => (str o mk_char) c
-        | NONE => error "Illegal character expression";
+        | NONE => nerror thm "Illegal character expression";
   in (2, pretty) end;
 
 fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 target =
   let
     val mk_numeral = #pretty_numeral (pr_pretty target);
-    fun pretty _ _ _ [(t, _)] =
-      (str o mk_numeral unbounded o implode_numeral negative c_pls c_min c_bit0 c_bit1) t;
+    fun pretty _ thm _ _ _ [(t, _)] =
+      (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
   in (1, pretty) end;
 
 fun pretty_message c_char c_nibbles c_nil c_cons target =
@@ -1764,12 +1767,12 @@
     val pretty_ops = pr_pretty target;
     val mk_char = #pretty_char pretty_ops;
     val mk_string = #pretty_string pretty_ops;
-    fun pretty pr vars fxy [(t, _)] =
+    fun pretty _ thm _ _ _ [(t, _)] =
       case implode_list c_nil c_cons t
        of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
            of SOME p => p
-            | NONE => error "Illegal message expression")
-        | NONE => error "Illegal message expression";
+            | NONE => nerror thm "Illegal message expression")
+        | NONE => nerror thm "Illegal message expression";
   in (1, pretty) end;
 
 fun pretty_imperative_monad_bind bind' return' unit' =
@@ -1800,26 +1803,21 @@
           | _ => force t;
     fun tr_bind ts = (dummy_name, dummy_type)
       `|-> ICase (((IVar dummy_name, dummy_type), [(unitt, tr_bind' ts)]), dummy_case_term);
-    fun pretty pr vars fxy ts = pr vars fxy (tr_bind ts);
+    fun pretty pr thm pat vars fxy ts = pr vars fxy (tr_bind ts);
   in (2, pretty) end;
 
-fun no_bindings x = (Option.map o apsnd)
-  (fn pretty => fn pr => fn vars => pretty (pr vars)) x;
-
 end; (*local*)
 
 
-(** serializer interfaces **)
+(** serializer use cases **)
 
 (* evaluation *)
 
-fun eval_serializer module [] = serialize_ml
-  (use_text (1, "code to be evaluated") Output.ml_output false) 
-  (K Pretty.chunks) pr_sml_stmt
+fun code_antiq_serializer module [] = serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt
   (fn SOME s => fn cs => SOME ("let\n" ^ s ^ "\nin fn () => " ^ enclose "(" ")" (commas cs) ^ " end"))
   (SOME "Isabelle_Eval");
 
-fun sml_code_of thy program cs = mount_serializer thy (SOME eval_serializer) target_SML NONE [] program cs String
+fun sml_code_of thy program cs = mount_serializer thy (SOME code_antiq_serializer) target_SML NONE [] program cs (String [])
   |> the;
 
 fun eval eval'' term_of reff thy ct args =
@@ -1843,16 +1841,61 @@
 fun eval_term reff = eval CodeThingol.eval_term I reff;
 
 
-(* presentation *)
+(* instrumentalization by antiquotation *)
 
-fun code_of thy target module_name cs =
+fun ml_code_antiq (ctxt, args) = 
+  let
+    val thy = Context.theory_of ctxt;
+    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
+    val cs = map (CodeUnit.check_const thy) ts;
+    val (cs', program) = CodeThingol.consts_program thy cs;
+    val s = sml_code_of thy program cs' ^ " ()";
+  in (("codevals", s), (ctxt', args')) end;
+
+
+(* code presentation *)
+
+fun code_of thy target module_name cs stmt_names =
   let
     val (cs', program) = CodeThingol.consts_program thy cs;
   in
-    string (serialize thy target (SOME module_name) [] program cs')
+    string stmt_names (serialize thy target (SOME module_name) [] program cs')
   end;
 
 
+(* code generation *)
+
+fun read_const_exprs thy cs =
+  let
+    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
+    val (cs3, program) = CodeThingol.consts_program thy cs2;
+    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
+    val cs5 = map_filter
+      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
+  in fold (insert (op =)) cs5 cs1 end;
+
+fun cached_program thy = 
+  let
+    val program = CodeThingol.cached_program thy;
+  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
+
+fun export_code thy cs seris =
+  let
+    val (cs', program) = if null cs then cached_program thy
+      else CodeThingol.consts_program thy cs;
+    fun mk_seri_dest dest = case dest
+     of NONE => compile
+      | SOME "-" => export
+      | SOME f => file (Path.explode f)
+    val _ = map (fn (((target, module), dest), args) =>
+      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
+  in () end;
+
+fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
+
+
+(** serializer data **)
+
 (* infix syntax *)
 
 datatype 'a mixfix =
@@ -1869,11 +1912,7 @@
       | fillin pr (Arg fxy :: mfx) (a :: args) =
           (pr fxy o prep_arg) a :: fillin pr mfx args
       | fillin pr (Pretty p :: mfx) args =
-          p :: fillin pr mfx args
-      | fillin _ [] _ =
-          error ("Inconsistent mixfix: too many arguments")
-      | fillin _ _ [] =
-          error ("Inconsistent mixfix: too less arguments");
+          p :: fillin pr mfx args;
   in
     (i, fn pr => fn fixity_ctxt => fn args =>
       gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
@@ -1960,6 +1999,9 @@
            (Symtab.delete_safe tyco')
   end;
 
+fun simple_const_syntax x = (Option.map o apsnd)
+  (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
+
 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
   let
     val c = prep_const thy raw_c;
@@ -2019,7 +2061,7 @@
     |> gen_add_syntax_const (K I) target_Haskell c_run
           (SOME (pretty_haskell_monad c_bind'))
     |> gen_add_syntax_const (K I) target_Haskell c_bind
-          (no_bindings (SOME (parse_infix fst (L, 1) ">>=")))
+          (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
   else
     thy
     |> gen_add_syntax_const (K I) target c_bind
@@ -2097,11 +2139,11 @@
 val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
 
 fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
-fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o no_bindings);
+fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
 
 fun add_undefined target undef target_undefined thy =
   let
-    fun pr _ _ _ _ = str target_undefined;
+    fun pr _ _ _ _ _ _ = str target_undefined;
   in
     thy
     |> add_syntax_const target undef (SOME (~1, pr))
@@ -2164,49 +2206,8 @@
   end;
 
 
-(** code generation at a glance **)
 
-fun read_const_exprs thy cs =
-  let
-    val (cs1, cs2) = CodeName.read_const_exprs thy cs;
-    val (cs3, program) = CodeThingol.consts_program thy cs2;
-    val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
-    val cs5 = map_filter
-      (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
-  in fold (insert (op =)) cs5 cs1 end;
-
-fun cached_program thy = 
-  let
-    val program = CodeThingol.cached_program thy;
-  in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
-
-fun code thy cs seris =
-  let
-    val (cs', program) = if null cs
-      then cached_program thy
-      else CodeThingol.consts_program thy cs;
-    fun mk_seri_dest dest = case dest
-     of NONE => compile
-      | SOME "-" => write
-      | SOME f => file (Path.explode f)
-    val _ = map (fn (((target, module), dest), args) =>
-      (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
-  in () end;
-
-fun sml_of thy cs = 
-  let
-    val (cs', program) = CodeThingol.consts_program thy cs;
-  in sml_code_of thy program cs' ^ " ()" end;
-
-fun code_antiq (ctxt, args) = 
-  let
-    val thy = Context.theory_of ctxt;
-    val (ts, (ctxt', args')) = Scan.repeat1 Args.term (ctxt, args);
-    val cs = map (CodeUnit.check_const thy) ts;
-    val s = sml_of thy cs;
-  in (("codevals", s), (ctxt', args')) end;
-
-fun export_code_cmd raw_cs seris thy = code thy (read_const_exprs thy raw_cs) seris;
+(** Isar setup **)
 
 val (inK, module_nameK, fileK) = ("in", "module_name", "file");
 
@@ -2218,9 +2219,6 @@
      -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
   ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
 
-
-(** Isar setup **)
-
 val _ = OuterSyntax.keywords [infixK, infixlK, infixrK, inK, module_nameK, fileK];
 
 val _ =
@@ -2251,7 +2249,7 @@
   OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
     parse_multi_syntax P.term (parse_syntax fst)
     >> (Toplevel.theory oo fold) (fn (target, syns) =>
-          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (no_bindings syn)) syns)
+          fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
   );
 
 val _ =
@@ -2296,7 +2294,7 @@
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
 
-val _ = ML_Context.value_antiq "code" code_antiq;
+val _ = ML_Context.value_antiq "code" ml_code_antiq;
 
 
 (* serializer setup, including serializer defaults *)