src/Tools/code/code_thingol.ML

   val project_code: bool (*delete empty funs*)
     -> string list (*hidden*) -> string list option (*selected*)
     -> code -> code;
   val empty_funs: code -> string list;
   val is_cons: code -> string -> bool;
-  val add_eval_def: string (*bind name*) * iterm -> code -> code;
+  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
 
   val ensure_def: (string -> string) -> (transact -> def * transact) -> string
     -> string -> transact -> transact;
   val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
 end;

   | Classinst of (class * (string * (vname * sort) list))
         * ((class * (string * (string * dict list list))) list
       * (string * iterm) list);
 
 type code = def Graph.T;
-type transact = Graph.key option * code;
 
 
 (* abstract code *)
 
 val empty_code = Graph.empty : code; (*read: "depends on"*)

       I;
 
 
 (* transaction protocol *)
 
+type transact = Graph.key option * code;
+
 fun ensure_def labelled_name defgen msg name (dep, code) =
   let
     val msg' = (case dep
      of NONE => msg
       | SOME dep => msg ^ ", required for " ^ labelled_name dep);

 fun start_transact f code =
   (NONE, code)
   |> f
   |-> (fn x => fn (_, code) => (x, code));
 
-fun add_eval_def (name, t) code =
+fun add_eval_def (name, (t, ty)) code =
   code
-  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
+  |> Graph.new_node (name, Fun ([([], t)], ([], ty)))
   |> fold (curry Graph.add_edge name) (Graph.keys code);
 
 end; (*struct*)