aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/rules.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/rules.ml')
-rw-r--r--plugins/firstorder/rules.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index fc31ee6fc..75d69099a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -45,7 +45,7 @@ let wrap n b continue seq gls=
add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
continue seq2 gls
-let id_of_global=function
+let basename_of_global=function
VarRef id->id
| _->assert false