# HG changeset patch # User haftmann # Date 1474869414 -7200 # Node ID 429cfc5f2559fae103e59d20d04e9276982030ac # Parent 559f0882d6a6cb4c0abd82d082045397edfe1176 more warning comments diff -r 559f0882d6a6 -r 429cfc5f2559 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Tools/lin_arith.ML Mon Sep 26 07:56:54 2016 +0200 @@ -178,7 +178,7 @@ in which case dest_numeral raises TERM; hence all the handles below. Same for Suc-terms that turn out not to be numerals - although the simplifier should eliminate those anyway ...*) - | demult (t as Const ("Num.numeral_class.numeral", _) $ n, m) = + | demult (t as Const ("Num.numeral_class.numeral", _) (*DYNAMIC BINDING!*) $ n, m) = ((NONE, Rat.mult m (Rat.of_int (HOLogic.dest_numeral n))) handle TERM _ => (SOME t, m)) | demult (t as Const (@{const_name Suc}, _) $ _, m) = @@ -207,7 +207,7 @@ pi | poly (Const (@{const_name Groups.one}, _), m, (p, i)) = (p, Rat.add i m) - | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) $ t, m, pi as (p, i)) = + | poly (all as Const ("Num.numeral_class.numeral", Type(_,[_,_])) (*DYNAMIC BINDING!*) $ t, m, pi as (p, i)) = (let val k = HOLogic.dest_numeral t in (p, Rat.add i (Rat.mult m (Rat.of_int k))) end handle TERM _ => add_atom all m pi) @@ -444,7 +444,7 @@ SOME [(Ts, subgoal1), (split_type :: Ts, subgoal2)] end (* ?P (nat ?i) = ((ALL n. ?i = of_nat n --> ?P n) & (?i < 0 --> ?P 0)) *) - | (Const ("Int.nat", _), [t1]) => + | (Const ("Int.nat", _), (*DYNAMIC BINDING!*) [t1]) => let val rev_terms = rev terms val zero_int = Const (@{const_name Groups.zero}, HOLogic.intT) @@ -467,7 +467,7 @@ (* ?P ((?n::nat) mod (numeral ?k)) = ((numeral ?k = 0 --> ?P ?n) & (~ (numeral ?k = 0) --> (ALL i j. j < numeral ?k --> ?n = numeral ?k * i + j --> ?P j))) *) - | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), [t1, t2]) => + | (Const ("Divides.div_class.mod", Type ("fun", [@{typ nat}, _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms val zero = Const (@{const_name Groups.zero}, split_type) @@ -537,7 +537,7 @@ (ALL i j. numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P j))) *) | (Const ("Divides.div_class.mod", - Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) => + Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms val zero = Const (@{const_name Groups.zero}, split_type) @@ -591,7 +591,7 @@ (ALL i j. numeral ?k < j & j <= 0 & ?n = numeral ?k * i + j --> ?P i))) *) | (Const (@{const_name Rings.divide}, - Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) => + Type ("fun", [Type ("Int.int", []), _])), (*DYNAMIC BINDING!*) [t1, t2]) => let val rev_terms = rev terms val zero = Const (@{const_name Groups.zero}, split_type)