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