# HG changeset patch
# User wenzelm
# Date 1208012450 -7200
# Node ID 80384c1d16905b453d85c49e04e44d448715238b
# Parent  149f80f27c848ba5dae1431dc9dc0d31582def66
removed unnecessary Goal.close_result;

diff -r 149f80f27c84 -r 80384c1d1690 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Apr 12 17:00:48 2008 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sat Apr 12 17:00:50 2008 +0200
@@ -119,7 +119,6 @@
     (*thm definition*)
     val result = th''
       |> PureThy.name_thm true true ""
-      |> Goal.close_result
       |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
       |> PureThy.name_thm true true name;