aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/recdef.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/recdef.ml')
-rw-r--r--plugins/funind/recdef.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 68c5e16ae..7b77afd07 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -73,7 +73,7 @@ let def_of_const t =
| _ -> assert false)
with _ ->
anomaly ("Cannot find definition of constant "^
- (Id.to_string (id_of_label (con_label sp))))
+ (Id.to_string (Label.to_id (con_label sp))))
)
|_ -> assert false