# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 59753d5448e0b68964dff75fd3fd64c2657710d9
# Parent  b81127eb79f3af12c9cfb73802529accb804f898
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

diff -r b81127eb79f3 -r 59753d5448e0 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