| changeset 67710 | cc2db3239932 |
| parent 67329 | eabcd2e2bc9b |
| child 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/simpdata.ML Fri Feb 23 17:59:57 2018 +0100 +++ b/src/HOL/Tools/simpdata.ML Fri Feb 23 19:25:37 2018 +0100 @@ -50,7 +50,7 @@ | _ => th RS @{thm Eq_TrueI}) fun mk_eq_True (_: Proof.context) r = - SOME (r RS @{thm meta_eq_to_obj_eq} RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; + SOME (HOLogic.mk_obj_eq r RS @{thm Eq_TrueI}) handle Thm.THM _ => NONE; (* Produce theorems of the form (P1 =simp=> ... =simp=> Pn => x == y) ==> (P1 =simp=> ... =simp=> Pn => x = y)