# HG changeset patch
# User wenzelm
# Date 1343415524 -7200
# Node ID 04e1299311810a1dc5a4e9762fb4a7d5740bd15c
# Parent  f6d6d58fa318e0f8c9c26f8af0019a75597551f5
unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;

diff -r f6d6d58fa318 -r 04e129931181 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- 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)