more robust bundle_name: avoid assumptions about identifier, keywords etc.;

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Dec 03 14:04:38 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Dec 03 15:22:27 2014 +0100
@@ -221,7 +221,8 @@
 
     val thy = Proof_Context.theory_of lthy
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
-    val pointer = Token.explode (Thy_Header.get_keywords thy) Position.none bundle_name
+    val pointer =
+      Token.explode (Thy_Header.get_keywords thy) Position.none (cartouche bundle_name)
     val restore_lifting_att = 
       ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
@@ -920,7 +921,8 @@
 
 val lifting_restore_internal_attribute_setup =
   Attrib.setup @{binding lifting_restore_internal}
-     (Scan.lift Args.name >> (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
+    (Scan.lift Parse.cartouche >>
+      (fn name => Thm.declaration_attribute (K (lifting_restore_internal name))))
     "restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users"
 
 val _ = Theory.setup lifting_restore_internal_attribute_setup 
@@ -969,7 +971,7 @@
     case bundle of
       [(_, [arg_src])] => 
         let
-          val (name, _) = Token.syntax (Scan.lift Args.name) arg_src ctxt
+          val (name, _) = Token.syntax (Scan.lift Parse.cartouche) arg_src ctxt
             handle ERROR _ => error "The provided bundle is not a lifting bundle."
         in name end
       | _ => error "The provided bundle is not a lifting bundle."