src/Pure/Isar/context_rules.ML
changeset 25979 3297781f8141
parent 23227 96f86d377dd9
child 26435 bdce320cd426
--- a/src/Pure/Isar/context_rules.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -204,9 +204,9 @@
 
 (* concrete syntax *)
 
-fun add_args a b c x = Attrib.syntax
+fun add_args a b c = Attrib.syntax
   (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat)
-    >> (fn (f, n) => f n)) x;
+    >> (fn (f, n) => f n));
 
 val rule_atts =
  [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"),