--- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Mar 10 15:30:29 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Mar 10 16:30:07 2014 +0100
@@ -223,7 +223,7 @@
val dummy_thm = Thm.transfer thy Drule.dummy_thm
val pointer = Outer_Syntax.scan Position.none bundle_name
val restore_lifting_att =
- ([dummy_thm], [Args.src (("Lifting.lifting_restore_internal", pointer), Position.none)])
+ ([dummy_thm], [Args.src ("Lifting.lifting_restore_internal", Position.none) pointer])
in
lthy
|> Local_Theory.declaration {syntax = false, pervasive = true}
@@ -959,7 +959,7 @@
case bundle of
[(_, [arg_src])] =>
(let
- val ((_, tokens), _) = Args.dest_src arg_src
+ val tokens = Args.args_of_src arg_src
in
(fst (Args.name tokens))
handle _ => error "The provided bundle is not a lifting bundle."