Added Streicher's K axiom.

[helm.git] / helm / software / lambda-delta / common / library.ml

diff --git a/helm/software/lambda-delta/common/library.ml b/helm/software/lambda-delta/common/library.ml
index 61af9792127f9c900992e4e1e9bfe4f636fc9105..94ee60bd3f188564aebca8408f3a6139bd927a5b 100644 (file)
--- a/helm/software/lambda-delta/common/library.ml
+++ b/helm/software/lambda-delta/common/library.ml
@@ -119,7 +119,7 @@ let export_entity pp_term si g (a, u, b) =
       | Y.Void   -> assert false
    in
    let opts = if si then "si" else "" in
-   let shp = H.string_of_graph C.start g in
+   let shp = H.string_of_graph g in
    let attrs = ["hierarchy", shp; "options", opts] in
    tag root attrs ~contents out 0;
    close_out och