src/Tools/nbe.ML
changeset 59582 0fbed69ff081
parent 59153 b5e253703ebd
child 59586 ddf6deaadfe8
     1.1 --- a/src/Tools/nbe.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/Tools/nbe.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -589,7 +589,7 @@
     1.4  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
     1.5    (Thm.add_oracle (@{binding normalization_by_evaluation},
     1.6      fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) =>
     1.7 -      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (term_of ct) vs_ty_t deps))));
     1.8 +      mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (Thm.term_of ct) vs_ty_t deps))));
     1.9  
    1.10  fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct =
    1.11    raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct);