Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified goal_spec: default to first goal;
authorwenzelm
Fri, 13 Mar 2009 23:32:40 +0100
changeset 30514 9455ecc7796d
parent 30513 1796b8ea88aa
child 30515 bca05b17b618
simplified goal_spec: default to first goal;
src/Pure/Isar/args.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle