src/Tools/nbe.ML
changeset 43619 3803869014aa
parent 43329 84472e198515
child 44338 700008399ee5
     1.1 --- a/src/Tools/nbe.ML	Fri Jul 01 15:14:44 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Fri Jul 01 15:16:03 2011 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4  val get_triv_classes = map fst o Triv_Class_Data.get;
     1.5  
     1.6  val (_, triv_of_class) = Context.>>> (Context.map_theory_result
     1.7 -  (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
     1.8 +  (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
     1.9      Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
    1.10  
    1.11  in
    1.12 @@ -589,7 +589,7 @@
    1.13    in Thm.mk_binop eq lhs rhs end;
    1.14  
    1.15  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    1.16 -  (Thm.add_oracle (Binding.name "normalization_by_evaluation",
    1.17 +  (Thm.add_oracle (@{binding normalization_by_evaluation},
    1.18      fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
    1.19        mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
    1.20