diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Thu Jan 19 21:22:08 2006 +0100
@@ -23,7 +23,7 @@
   if ! quick_and_dirty then prop
   else error "Proof may be skipped in quick_and_dirty mode only!";
 
-val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
+val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
 
 
 (* basic cheating *)