try to detect assumptions of transfer rules that are in a shape of a transfer rule

--- a/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Tools/transfer.ML	Mon May 13 12:13:24 2013 +0200
@@ -111,10 +111,25 @@
   in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end
 
 (* Conversion to preprocess a transfer rule *)
+fun strip_args n = funpow n (fst o dest_comb)
+
+fun safe_Rel_conv ct =
+  let
+    val head = ct |> term_of |> HOLogic.dest_Trueprop |> strip_args 2
+    fun is_known (Const (s, _)) = (s = @{const_name DOM})
+      | is_known _ = false
+  in
+    if not (is_known head)
+      then HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv)) ct
+    else Conv.all_conv ct
+  end
+  handle TERM _ => Conv.all_conv ct
+;
+
 fun prep_conv ct = (
-      Conv.implies_conv Conv.all_conv prep_conv
+      Conv.implies_conv safe_Rel_conv prep_conv
       else_conv
-      HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))
+      safe_Rel_conv
       else_conv
       Conv.all_conv) ct
 

--- a/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
+++ b/src/HOL/Transfer.thy	Mon May 13 12:13:24 2013 +0200
@@ -103,6 +103,10 @@
   shows "Rel (A ===> B) (\<lambda>x. f x) (\<lambda>y. g y)"
   using assms unfolding Rel_def fun_rel_def by fast
 
+text {* Handling of domains *}
+
+definition DOM :: "('a => 'b => bool) => ('a => bool) => bool" where "DOM T R \<equiv> Domainp T = R"
+
 ML_file "Tools/transfer.ML"
 setup Transfer.setup