changeset 5610 | 377acd99d74c |
parent 5595 | d283d6120548 |
child 6917 | eba301caceea |
--- a/src/HOL/Integ/simproc.ML Mon Oct 05 10:15:01 1998 +0200 +++ b/src/HOL/Integ/simproc.ML Mon Oct 05 10:19:21 1998 +0200 @@ -28,8 +28,7 @@ structure Int_Cancel_Data = struct val ss = HOL_ss - val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq - fun mk_meta_eq r = r RS eq_reflection + val eq_reflection = eq_reflection val thy = IntDef.thy val T = Type ("IntDef.int", [])