--- a/src/HOL/Transfer.thy Fri Apr 11 22:53:47 2014 +0200
+++ b/src/HOL/Transfer.thy Fri Apr 11 23:22:00 2014 +0200
@@ -249,11 +249,6 @@
setup Transfer.setup
declare refl [transfer_rule]
-ML_file "Tools/Transfer/transfer_bnf.ML"
-
-declare pred_fun_def [simp]
-declare rel_fun_eq [relator_eq]
-
hide_const (open) Rel
context
@@ -366,8 +361,19 @@
unfolding bi_unique_alt_def bi_total_alt_def
by (blast intro: right_unique_fun left_unique_fun)
+end
+
+ML_file "Tools/Transfer/transfer_bnf.ML"
+
+declare pred_fun_def [simp]
+declare rel_fun_eq [relator_eq]
+
subsection {* Transfer rules *}
+context
+begin
+interpretation lifting_syntax .
+
lemma Domainp_forall_transfer [transfer_rule]:
assumes "right_total A"
shows "((A ===> op =) ===> op =)