removed unnecessary Goal.close_result;
authorwenzelm
Sat, 12 Apr 2008 17:00:50 +0200
changeset 26635 80384c1d1690
parent 26634 149f80f27c84
child 26636 65343a5ac627
removed unnecessary Goal.close_result;
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;