equal
deleted
inserted
replaced
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 in |
658 val [nthm1] = ProofContext.export ctxt' ctxt [nthm] |
658 Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1)) |
659 in |
659 |> singleton (ProofContext.export ctxt' ctxt) |
660 nthm1 |
|
661 end; |
660 end; |
662 |
661 |
663 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux |
662 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux |
664 |
663 |
665 end; (* structure *) |
664 end; (* structure *) |