src/HOL/Library/Eval.thy

 val eval_ref = ref (NONE : term option);
 
 end;
 *}
 
-oracle eval_oracle ("term * CodeThingol.code * CodeThingol.iterm * CodeThingol.itype * cterm") = {* fn thy => fn (t0, code, t, ty, ct) => 
+oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
+{* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
 let
   val _ = (Term.map_types o Term.map_atyps) (fn _ =>
     error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
     t0;
 in Logic.mk_equals (t0, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end;

 structure Eval : EVAL =
 struct
 
 open Eval;
 
-fun eval_invoke thy t0 code (t, ty) _ ct = eval_oracle thy (t0, code, t, ty, ct);
+fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
 
 fun eval_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
     val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;