# 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)