# 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;