--- 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)) --
--- 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;
--- 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)
--- 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) >>
--- 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
--- 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;
--- 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"),