src/Tools/Code/code_runtime.ML

   in
     Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct)
   end;
 
 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "holds_by_evaluation",
+  (Thm.add_oracle (@{binding holds_by_evaluation},
   fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
 
 fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
   raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
 

 
 (** Isar setup **)
 
 val _ =
   Context.>> (Context.map_theory
-    (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
+    (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
 
 local
 
 val datatypesK = "datatypes";
 val functionsK = "functions";