--- a/src/HOL/Tools/lin_arith.ML Sun May 18 15:04:20 2008 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sun May 18 15:04:22 2008 +0200
@@ -140,7 +140,7 @@
(* Decomposition of terms *)
(*internal representation of linear (in-)equations*)
-type decompT =
+type decomp =
((term * Rat.rat) list * Rat.rat * string * (term * Rat.rat) list * Rat.rat * bool);
fun nT (Type ("fun", [N, _])) = (N = HOLogic.natT)
@@ -272,7 +272,7 @@
| allows_lin_arith sg discrete U =
(of_lin_arith_sort sg U, false);
-fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decompT option =
+fun decomp_typecheck (thy, discrete, inj_consts) (T : typ, xxx) : decomp option =
case T of
Type ("fun", [U, _]) =>
(case allows_lin_arith thy discrete U of
@@ -288,7 +288,7 @@
| negate NONE = NONE;
fun decomp_negation data
- ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decompT option =
+ ((Const ("Trueprop", _)) $ (Const (rel, T) $ lhs $ rhs)) : decomp option =
decomp_typecheck data (T, (rel, lhs, rhs))
| decomp_negation data ((Const ("Trueprop", _)) $
(Const ("Not", _) $ (Const (rel, T) $ lhs $ rhs))) =
@@ -296,7 +296,7 @@
| decomp_negation data _ =
NONE;
-fun decomp ctxt : term -> decompT option =
+fun decomp ctxt : term -> decomp option =
let
val thy = ProofContext.theory_of ctxt
val {discrete, inj_consts, ...} = get_arith_data ctxt