author | nipkow |
Sun, 09 Feb 2014 13:07:23 +0100 | |
changeset 55362 | 5e5c36b051af |
parent 55361 | d459a63ca42f |
child 55363 | b7c061e1d817 |
child 55365 | 9d5aba2baa4c |
child 55375 | d26d5f988d71 |
--- a/src/Provers/Arith/fast_lin_arith.ML Sat Feb 08 20:34:10 2014 +0100 +++ b/src/Provers/Arith/fast_lin_arith.ML Sun Feb 09 13:07:23 2014 +0100 @@ -763,7 +763,7 @@ (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params)) val params' = (more_names @ param_names) ~~ Ts in - trace_ex ctxt'' params' atoms (discr initems) n hist + () (*trace_ex ctxt'' params' atoms (discr initems) n hist*) end; NONE) end | refute [] js = SOME js