# HG changeset patch
# User wenzelm
# Date 1228992946 -3600
# Node ID a049c9816c24d24992eb88bb89a6f7977ba0eb6d
# Parent  c7c0dd65159a9bfbbbb0950cf09dadc4c24d6e77
add_typedef: unfold set_def in tactical proof as well;

diff -r c7c0dd65159a -r a049c9816c24 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Dec 11 10:41:53 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 11 11:55:46 2008 +0100
@@ -197,9 +197,10 @@
     val name = the_default (#1 typ) opt_name;
     val ((set, goal, _, set_def, typedef_result), thy') =
       prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
-    val non_empty = Goal.prove_global thy' [] [] goal (K tac)
-      handle ERROR msg => cat_error msg
-        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+    val non_empty =
+      Goal.prove_global thy' [] [] goal (fn _ => rewrite_goals_tac (the_list set_def) THEN tac)
+        handle ERROR msg => cat_error msg
+          ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
   in typedef_result non_empty thy' end;