--- 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