changeset 72452 | 9017dfa56367 |
parent 70473 | 9179e7a98196 |
child 74152 | 069f6b2c5a07 |
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Oct 12 07:25:38 2020 +0000 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Oct 12 07:25:38 2020 +0000 @@ -968,7 +968,7 @@ fun pointer_of_bundle_name bundle_name ctxt = let - val bundle = Bundle.get_bundle_cmd ctxt bundle_name + val bundle = Bundle.read ctxt bundle_name fun err () = error "The provided bundle is not a lifting bundle" in (case bundle of