1234     in

  1234     in

  1235       EVERY1 [rtac rule, rtac rthm']

  1235       EVERY1 [rtac rule, rtac rthm']

  1236     end) lthy

  1236     end) lthy

  1237 *}

  1237 *}

  1238 

  1238 

  1239 ML {*

  1242 ML {*

  1240 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)

  1243 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)

  1241 fun lift_tac lthy rthm rel_eqv rty quot defs =

  1244 fun lift_tac lthy rthm rel_eqv rty quot defs =

  1242   ObjectLogic.full_atomize_tac

  1245   ObjectLogic.full_atomize_tac

  1243   THEN' gen_frees_tac lthy

  1246   THEN' gen_frees_tac lthy