--- a/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Tue Aug 19 23:17:51 2014 +0200
@@ -13,7 +13,8 @@
(binding * mixfix) -> typ -> term -> thm -> thm list -> local_theory -> local_theory
val lift_def_cmd:
- (binding * string option * mixfix) * string * (Facts.ref * Args.src list) list -> local_theory -> Proof.state
+ (binding * string option * mixfix) * string * (Facts.ref * Token.src list) list ->
+ local_theory -> Proof.state
val can_generate_code_cert: thm -> bool
end