src/Tools/nbe.ML
changeset 56245 84fc7dfa3cd4
parent 55757 9fc71814b8c1
child 56920 d651b944c67e
     1.1 --- a/src/Tools/nbe.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Tools/nbe.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -586,7 +586,7 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of ctxt;
     1.6      val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
     1.7 -    val eq = Thm.cterm_of thy (Term.Const ("==", ty --> ty --> propT));
     1.8 +    val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
     1.9      val rhs = Thm.cterm_of thy raw_rhs;
    1.10    in Thm.mk_binop eq lhs rhs end;
    1.11