equal
deleted
inserted
replaced
4153 in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end; |
4153 in HOLogic.mk_Trueprop (HOLogic.mk_eq (t, eval t)) end; |
4154 |
4154 |
4155 in |
4155 in |
4156 |
4156 |
4157 fn (ctxt, alternative, ty, ps, ct) => |
4157 fn (ctxt, alternative, ty, ps, ct) => |
4158 Proof_Context.cterm_of ctxt |
4158 Thm.cterm_of ctxt |
4159 (frpar_procedure alternative ty ps (Thm.term_of ct)) |
4159 (frpar_procedure alternative ty ps (Thm.term_of ct)) |
4160 |
4160 |
4161 end |
4161 end |
4162 *} |
4162 *} |
4163 |
4163 |