# HG changeset patch
# User wenzelm
# Date 1211115862 -7200
# Node ID 87e4208700d1f951f58bb25f2b71efc6032c77ed
# Parent  fe007ee497c1baffa7cd761593a4cd724ac032fc
renamed type decompT to decomp;

diff -r fe007ee497c1 -r 87e4208700d1 src/HOL/Tools/lin_arith.ML
--- 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