# HG changeset patch
# User wenzelm
# Date 1201363718 -3600
# Node ID 3297781f814163641c443730864c2ad42cc255ad
# Parent  8ba1eba8d058b88c435443589d8be22f99f90700
tuned attribute syntax -- no need for eta-expansion;

diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -191,7 +191,7 @@
 
 in
 
-fun att_syntax src = src |> Attrib.syntax
+val att_syntax = Attrib.syntax
   (Scan.lift (Args.$$$ delN >> K del) ||
     ((keyword2 semiringN opsN |-- terms) --
      (keyword2 semiringN rulesN |-- thms)) --
diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -77,7 +77,7 @@
 fun optional scan = Scan.optional scan [];
 
 in
-fun att_syntax src = src |> Attrib.syntax
+val att_syntax = Attrib.syntax
  ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
   optional (keyword constsN |-- terms) >> add)
 end;
diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -122,7 +122,7 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-fun att_syntax src = src |> Attrib.syntax
+val att_syntax = Attrib.syntax
     ((keyword minfN |-- thms)
      -- (keyword pinfN |-- thms)
      -- (keyword nmiN |-- thms)
diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/Tools/Qelim/langford_data.ML
--- a/src/HOL/Tools/Qelim/langford_data.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -85,7 +85,7 @@
 val terms = thms >> map Drule.dest_term;
 in
 
-fun att_syntax src = src |> Attrib.syntax
+val att_syntax = Attrib.syntax
     ((keyword qeN |-- thms)
      -- (keyword gatherN |-- thms)
      -- (keyword atomsN |-- terms) >> 
diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/Tools/split_rule.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -141,11 +141,11 @@
 
 (* FIXME dynamically scoped due to Args.name/pair_tac *)
 
-fun split_format x = Attrib.syntax
+val split_format = Attrib.syntax
   (Scan.lift (Args.parens (Args.$$$ "complete"))
     >> K (Thm.rule_attribute (K complete_split_rule)) ||
   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
-    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss)))) x;
+    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss))));
 
 val setup =
   Attrib.add_attributes
diff -r 8ba1eba8d058 -r 3297781f8141 src/HOL/ex/reflection_data.ML
--- a/src/HOL/ex/reflection_data.ML	Sat Jan 26 17:08:36 2008 +0100
+++ b/src/HOL/ex/reflection_data.ML	Sat Jan 26 17:08:38 2008 +0100
@@ -56,7 +56,7 @@
 fun optional scan = Scan.optional scan [];
 
 in
-fun att_syntax src = src |> Attrib.syntax
+val att_syntax = Attrib.syntax
  ((Scan.lift (Args.$$$ "del") |-- thms) >> del ||
   optional (keyword addN |-- thms) >> add)
 end;
diff -r 8ba1eba8d058 -r 3297781f8141 src/Pure/Isar/context_rules.ML
--- 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"),