diff -r 39b931e00ba9 -r a32700e45ab3 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 18:19:20 2009 +0100
+++ b/src/Tools/Compute_Oracle/compute.ML	Thu Mar 05 19:48:02 2009 +0100
@@ -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 ("compute", fn (thy, hyps, shyps, prop) =>
+  (Thm.add_oracle (Binding.name "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