src/HOL/Matrix/Compute_Oracle/compute.ML

 fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab
 
 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
 
 val (_, export_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
+  (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
     let
         val shyptab = add_shyps shyps Sorttab.empty
         fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab
         fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab
         fun has_witness s = not (null (Sign.witness_sorts thy [] [s]))