89 ML {*

    90 val no_vars = Thm.rule_attribute (fn context => fn th =>

    91   let

    92     val ctxt = Variable.set_body false (Context.proof_of context);

    93     val ((_, [th']), _) = Variable.import true [th] ctxt;

    94   in th' end);

    95 *}