aboutsummaryrefslogtreecommitdiff
path: root/contrib/first-order
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/first-order')
-rw-r--r--contrib/first-order/sequent.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index c1175a4d9c..fd5972fb74 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -278,7 +278,7 @@ let create_with_auto_hints l depth gl=
let h dbname=
let hdb=
try
- Util.Stringmap.find dbname !searchtable
+ searchtable_map dbname
with Not_found->
error ("Firstorder: "^dbname^" : No such Hint database") in
Hint_db.iter g hdb in