renamed type decompT to decomp;
authorwenzelm
Sun, 18 May 2008 15:04:22 +0200
changeset 26942 87e4208700d1
parent 26941 fe007ee497c1
child 26943 aec0d97a01c4
renamed type decompT to decomp;
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