MK_USING
markerSyntax.MK_USING : thm -> thm
Encodes a theorem so it can be ASSUME_TAC-ed into a goal.
A call to MK_USING th encodes th in such a way that it can safely be
the argument to ASSUME_TAC, and detectable by other tactics operating
on the resulting goal as a theorem that might be worthy of notice.
Failure
Fails if the theorem has no hypotheses, is polymorphic, and cannot be
found by reverse lookup in the theorem database (using DB.revlookup).