1open HolKernel Parse boolLib Datatype 2 3val _ = new_theory "foo" 4 5val _ = Hol_datatype`foo = Success | Failure` 6 7val _ = export_theory() 8