--- a/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Aug 27 17:23:57 2010 +0200
+++ b/src/HOL/Matrix/Compute_Oracle/compute.ML Fri Aug 27 17:59:40 2010 +0200
@@ -371,7 +371,7 @@
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