src/Pure/codegen.ML
changeset 30288 a32700e45ab3
parent 29270 0eade173f77e
child 30364 577edc39b501
     1.1 --- a/src/Pure/codegen.ML	Thu Mar 05 18:19:20 2009 +0100
     1.2 +++ b/src/Pure/codegen.ML	Thu Mar 05 19:48:02 2009 +0100
     1.3 @@ -938,7 +938,7 @@
     1.4    in e () end;
     1.5  
     1.6  val (_, evaluation_conv) = Context.>>> (Context.map_theory_result
     1.7 -  (Thm.add_oracle ("evaluation", fn ct =>
     1.8 +  (Thm.add_oracle (Binding.name "evaluation", fn ct =>
     1.9      let
    1.10        val thy = Thm.theory_of_cterm ct;
    1.11        val t = Thm.term_of ct;