src/Tools/nbe.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59621 291934bac95e
     1.1 --- a/src/Tools/nbe.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/Tools/nbe.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -581,7 +581,7 @@
     1.4  fun mk_equals ctxt lhs raw_rhs =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt;
     1.7 -    val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
     1.8 +    val ty = Thm.typ_of_cterm lhs;
     1.9      val eq = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, ty --> ty --> propT));
    1.10      val rhs = Thm.cterm_of thy raw_rhs;
    1.11    in Thm.mk_binop eq lhs rhs end;