# HG changeset patch
# User wenzelm
# Date 1417616547 -3600
# Node ID f982f3072d7957524a6c9c29c40a6e03ecc459c6
# Parent  88b0b1f28adc4bd4c768b91b3f1953ad5a62f267
more robust bundle_name: avoid assumptions about identifier, keywords etc.;

diff -r 88b0b1f28adc -r f982f3072d79 src/HOL/Tools/Lifting/lifting_setup.ML
--- 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."