diff -r 25501ba956ac -r 88b0b1f28adc src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Wed Dec 03 11:50:58 2014 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Dec 03 14:04:38 2014 +0100 @@ -221,7 +221,7 @@ val thy = Proof_Context.theory_of lthy val dummy_thm = Thm.transfer thy Drule.dummy_thm - val pointer = Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none bundle_name + val pointer = Token.explode (Thy_Header.get_keywords thy) Position.none bundle_name val restore_lifting_att = ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer]) in