src/HOL/Matrix/Compute_Oracle/compute.ML
changeset 38808 89ae86205739
parent 37872 d83659570337
child 40314 b5ec88d9ac03
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:23:57 2010 +0200
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/compute.ML	Fri Aug 27 17:59:40 2010 +0200
     1.3 @@ -371,7 +371,7 @@
     1.4  fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty))
     1.5  
     1.6  val (_, export_oracle) = Context.>>> (Context.map_theory_result
     1.7 -  (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) =>
     1.8 +  (Thm.add_oracle (@{binding compute}, fn (thy, hyps, shyps, prop) =>
     1.9      let
    1.10          val shyptab = add_shyps shyps Sorttab.empty
    1.11          fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab