equal
deleted
inserted
replaced
651 (* An Attribute which automatically constructs the qthm *) |
651 (* An Attribute which automatically constructs the qthm *) |
652 fun lifted_attrib_aux context thm = |
652 fun lifted_attrib_aux context thm = |
653 let |
653 let |
654 val ctxt = Context.proof_of context |
654 val ctxt = Context.proof_of context |
655 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt |
655 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt |
656 val goal = (quotient_lift_all ctxt o prop_of) thm' |
656 val goal = (quotient_lift_all ctxt' o prop_of) thm' |
657 val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1) |
657 val nthm = Goal.prove ctxt' [] [] goal (fn x => lift_tac ctxt' [thm] 1) |
658 val [nthm1] = ProofContext.export ctxt' ctxt [nthm] |
658 val [nthm1] = ProofContext.export ctxt' ctxt [nthm] |
659 in |
659 in |
660 nthm1 |
660 nthm1 |
661 end; |
661 end; |
662 |
662 |