removed unnecessary Goal.close_result;
authorwenzelm
Sat Apr 12 17:00:50 2008 +0200 (2008-04-12)
changeset 2663580384c1d1690
parent 26634 149f80f27c84
child 26636 65343a5ac627
removed unnecessary Goal.close_result;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Apr 12 17:00:48 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Apr 12 17:00:50 2008 +0200
     1.3 @@ -119,7 +119,6 @@
     1.4      (*thm definition*)
     1.5      val result = th''
     1.6        |> PureThy.name_thm true true ""
     1.7 -      |> Goal.close_result
     1.8        |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
     1.9        |> PureThy.name_thm true true name;
    1.10