# HG changeset patch
# User wenzelm
# Date 1236983560 -3600
# Node ID 9455ecc7796d8b54b1cbde9be508c9aad19c85f8
# Parent  1796b8ea88aaa20284998f4ec00daa05d245d695
simplified goal_spec: default to first goal;

diff -r 1796b8ea88aa -r 9455ecc7796d src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri Mar 13 21:25:15 2009 +0100
+++ b/src/Pure/Isar/args.ML	Fri Mar 13 23:32:40 2009 +0100
@@ -58,7 +58,7 @@
   val const: string context_parser
   val const_proper: string context_parser
   val bang_facts: thm list context_parser
-  val goal_spec: ((int -> tactic) -> tactic) -> ((int -> tactic) -> tactic) context_parser
+  val goal_spec: ((int -> tactic) -> tactic) context_parser
   val parse: token list parser
   val parse1: (string -> bool) -> token list parser
   val attribs: (string -> string) -> src list parser
@@ -233,7 +233,7 @@
   $$$ "!" >> K ALLGOALS;
 
 val goal = $$$ "[" |-- P.!!! (from_to --| $$$ "]");
-fun goal_spec def = Scan.lift (Scan.optional goal def);
+fun goal_spec x = Scan.lift (Scan.optional goal (fn tac => tac 1)) x;
 
 
 (* arguments within outer syntax *)