diff -r e6e3b20340be -r a6c3962ea907 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Sep 05 00:41:00 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Fri Sep 05 00:41:01 2014 +0200
@@ -6,6 +6,7 @@
 
 signature LIFTING_BNF =
 sig
+  val lifting_interpretation: string
 end
 
 structure Lifting_BNF : LIFTING_BNF =
@@ -15,6 +16,8 @@
 open BNF_Def
 open Transfer_BNF
 
+val lifting_interpretation = "lifting"
+
 (* Quotient map theorem *)
 
 fun Quotient_tac bnf ctxt i =
@@ -115,8 +118,8 @@
       snd (Local_Theory.notes notes lthy)
     end
 
-val _ = Theory.setup (bnf_interpretation
-  (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation))
+val _ = Theory.setup (bnf_interpretation lifting_interpretation
+  (bnf_only_type_ctr (BNF_Util.map_local_theory o lifting_bnf_interpretation))
   (bnf_only_type_ctr lifting_bnf_interpretation))
 
 end