src/Tools/code/code_target.ML

   val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
     -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;
   val assert_serializer: theory -> string -> string;
 
   val eval_verbose: bool ref;
-  val eval_term: theory -> (theory -> string -> string) -> CodeThingol.code
-    -> (string * 'a option ref) * CodeThingol.iterm -> string list -> 'a;
+  val eval_term: theory -> (string * 'a option ref) -> CodeThingol.code
+    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val code_width: int ref;
 
   val setup: theory -> theory;
 end;
 

      of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
     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 vars'' fxy) pat;
+    val pat' = Option.map (pr_term true vars'' fxy) pat;
   in (pr_bind' ((v', pat'), ty), vars'') end;
 
 
 (* list, char, string, numeral and monad abstract syntax transformations *)
 

     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs 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 false) fxy
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars

                            (insert (op =)) ts []);
                   in
                     concat (
                       [str definer, (str o deresolv) name]
                       @ (if null ts andalso null vs
-                           andalso not (ty = ITyVar "_")(*for evaluation*)
                          then [str ":", pr_typ NOBR ty]
                          else
                            pr_tyvars vs
                            @ map (pr_term true vars BR) ts)
                    @ [str "=", pr_term false vars NOBR t]

     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs 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 false) fxy
+    and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t') = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars

               | fish_parm _ NONE = NONE;
             fun fillup_parm _ (_, SOME v) = v
               | fillup_parm x (i, NONE) = x ^ string_of_int i;
             fun fish_parms vars eqs =
               let
-                val fished1 = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
-                val x = Name.variant (map_filter I fished1) "x";
-                val fished2 = map_index (fillup_parm x) fished1;
-                val fished3 = fold_rev (fn x => fn xs => Name.variant xs x :: xs) fished2 [];
-                val vars' = CodeName.intro_vars fished3 vars;
-              in map (CodeName.lookup_var vars') fished3 end;
+                val raw_fished = fold (map2 fish_parm) eqs (replicate (length (hd eqs)) NONE);
+                val x = Name.variant (map_filter I raw_fished) "x";
+                val fished = map_index (fillup_parm x) raw_fished;
+                val vars' = CodeName.intro_vars fished vars;
+              in map (CodeName.lookup_var vars') fished end;
             fun pr_eq (ts, t) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o const_syntax) c
                     then NONE else (SOME o NameSpace.base o deresolv) c)

                 else pr_app lhs vars fxy c_ts
             | NONE => pr_case vars fxy cases)
     and pr_app' lhs vars ((c, _), ts) =
       (str o deresolv) c :: map (pr_term lhs vars BR) ts
     and pr_app lhs vars = gen_pr_app pr_app' pr_term const_syntax labelled_name is_cons lhs vars
-    and pr_bind fxy = pr_bind_haskell (pr_term false) fxy
+    and pr_bind fxy = pr_bind_haskell pr_term fxy
     and pr_case vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, t) = CodeThingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars

 
 fun pretty_haskell_monad c_mbind c_kbind =
   let
     fun pretty pr vars fxy [(t, _)] =
       let
-        val pr_bind = pr_bind_haskell pr;
+        val pr_bind = pr_bind_haskell (K pr);
         fun pr_mbind (NONE, t) vars =
               (semicolon [pr vars NOBR t], vars)
           | pr_mbind (SOME (bind, true), t) vars = vars
               |> pr_bind NOBR bind
               |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])

     #> check_empty_funs
     #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
       (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   end;
 
-fun eval_term thy labelled_name code ((ref_name, reff), t) args =
+fun eval_term thy (ref_name, reff) code (t, ty) args =
   let
     val val_name = "Isabelle_Eval.EVAL.EVAL";
     val val_name' = "Isabelle_Eval.EVAL";
     val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
-    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
+    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
     fun eval code = (
       reff := NONE;
       seri (SOME [val_name]) code;
       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
         ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");

             ^ " (reference probably has been shadowed)")
         | SOME value => value
       );
   in
     code
-    |> CodeThingol.add_eval_def (val_name, t)
+    |> CodeThingol.add_eval_def (val_name, (t, ty))
     |> eval
   end;