# HG changeset patch
# User kuncar
# Date 1397251320 -7200
# Node ID 9bd56f2e4c10faa0ccff9d315ff8d6043ad267a1
# Parent  5dc66c358f7e68b9cccbd9455c078d2f9ff88855
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced

diff -r 5dc66c358f7e -r 9bd56f2e4c10 src/HOL/Transfer.thy
--- 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 =)