unpatch

#!/bin/sh

if test -z "$HOL2DK_DIR"
then
    echo "HOL2DK_DIR is not set"
    exit 1
fi

if test -z "$HOLLIGHT_DIR"
then
    echo "HOLLIGHT_DIR is not set"
    exit 1
fi

if test $# -ne 0
then
    echo "usage: `basename $0`"
    echo "unpatch the HOL-Light sources in $HOLLIGHT_DIR"
    exit 1
fi

restore() {
    if test -f $HOLLIGHT_DIR/$1-bak.ml
    then
        echo "mv$opt $HOLLIGHT_DIR/$1-bak.ml $HOLLIGHT_DIR/$1.ml ..."
        mv $HOLLIGHT_DIR/$1-bak.ml $HOLLIGHT_DIR/$1.ml
    else
        echo "$HOLLIGHT_DIR/lib-bak.ml does not exist"
    fi
}

remove() {
    echo "rm$opt $HOLLIGHT_DIR/$1.ml ..."
    rm$opt $HOLLIGHT_DIR/$1.ml
}

restore fusion
restore bool
restore equal
remove xnames