# HG changeset patch # User nipkow # Date 898073364 -7200 # Node ID 1f077d63a9091045ec8be74f553ad9a077b94a74 # Parent a1d0a6d555cd62a823367cf53cdf8a1b19f6cde4 Changed and changed back. diff -r a1d0a6d555cd -r 1f077d63a909 src/Pure/Thy/context.ML --- a/src/Pure/Thy/context.ML Wed Jun 17 10:48:38 1998 +0200 +++ b/src/Pure/Thy/context.ML Wed Jun 17 10:49:24 1998 +0200 @@ -82,8 +82,8 @@ (* shortcut goal commands *) -fun Goal s = Goals.goal (the_context ()) s; -fun Goalw thms s = Goals.goalw (the_context ()) thms s; +fun Goal s = Goals.atomic_goal (the_context ()) s; +fun Goalw thms s = Goals.atomic_goalw (the_context ()) thms s; end;