unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;

--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Fri Jul 27 19:57:23 2012 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Fri Jul 27 20:58:44 2012 +0200
@@ -132,7 +132,8 @@
 in
   fun beta_of_def thy def_thm =
       let
-        val (con, lam) = Logic.dest_equals (concl_of def_thm)
+        val (con, lam) =
+          Logic.dest_equals (Logic.unvarify_global (concl_of def_thm))
         val (args, rhs) = arglist lam
         val lhs = list_ccomb (con, args)
         val goal = mk_equals (lhs, rhs)