1215     in

  1215     in

  1216       EVERY1 [rtac rule, rtac rthm']

  1216       EVERY1 [rtac rule, rtac rthm']

  1217     end) lthy

  1217     end) lthy

  1218 *}

  1218 *}

  1219 

  1219 

  1220 ML {*

  1223 ML {*

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

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

  1222 fun lift_tac lthy rthm rel_eqv rty quot defs =

  1225 fun lift_tac lthy rthm rel_eqv rty quot defs =

  1223   ObjectLogic.full_atomize_tac

  1226   ObjectLogic.full_atomize_tac

  1224   THEN' gen_frees_tac lthy

  1227   THEN' gen_frees_tac lthy