added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file
authorblanchet
Thu, 12 May 2011 15:29:19 +0200
changeset 42744 59753d5448e0
parent 42743 b81127eb79f3
child 42745 b817c6f91a98
added "SMT." qualifier for constant to make it possible to reload "smt_monomorph.ML" from outside the "SMT" theory (for experiments) -- this is also consistent with the other SMT constants mentioned in this source file
src/HOL/Tools/SMT/smt_monomorph.ML
--- a/src/HOL/Tools/SMT/smt_monomorph.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_monomorph.ML	Thu May 12 15:29:19 2011 +0200
@@ -51,7 +51,7 @@
 
 fun collect_consts_if pred f =
   let
-    fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
+    fun collect (@{const SMT.trigger} $ p $ t) = collect_trigger p #> collect t
       | collect (t $ u) = collect t #> collect u
       | collect (Abs (_, _, t)) = collect t
       | collect (Const c) = if is_const pred c then f c else I