--- a/src/HOL/Tools/Presburger/presburger.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Jan 19 21:22:08 2006 +0100
@@ -14,7 +14,7 @@
sig
val presburger_tac : bool -> bool -> int -> tactic
val presburger_method : bool -> bool -> int -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
val trace : bool ref
end;
@@ -364,12 +364,12 @@
Method.insert_tac facts 1 THEN presburger_tac q a i)
val setup =
- [Method.add_method ("presburger",
- presburger_args presburger_method,
- "decision procedure for Presburger arithmetic"),
- ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
- {splits = splits, inj_consts = inj_consts, discrete = discrete,
- presburger = SOME (presburger_tac true true)})];
+ Method.add_method ("presburger",
+ presburger_args presburger_method,
+ "decision procedure for Presburger arithmetic") #>
+ ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
+ {splits = splits, inj_consts = inj_consts, discrete = discrete,
+ presburger = SOME (presburger_tac true true)});
end;