1structure HolKernel =
2struct
3  open HolKernel Logging
4  fun new_theory s = let
5    val _ = HolKernel.new_theory s
6    val _ = start_logging s
7    fun th {Thy,Tyop} =
8      case (Thy,Tyop) of
9          ("min", "fun") => ([], "->")
10        | ("min", "bool") => ([], "bool")
11        | _ => (["HOL4",Thy],Tyop)
12    fun ch {Thy,Name} =
13      case (Thy,Name) of
14          ("min", "=") => ([], "=")
15        | ("arithmetic", "NUMERAL") => (["Unwanted"],"id")
16        | _ => (["HOL4",Thy],Name)
17    val _ = set_tyop_name_handler th
18    val _ = set_const_name_handler ch
19  in () end
20
21  fun export_theory() = let
22    open Lib Theory
23    val directives = Logging.read_otdfile (current_theory() ^ ".otd")
24                                          handle IO.Io _ => []
25    fun prepare (nm, th) =
26      (if Lib.mem (DeleteProof, nm) directives
27       then Thm.delete_proof th else ();
28       if Lib.mem (SkipThm, nm) directives
29       then NONE else SOME th)
30    val defs' = List.mapPartial prepare (current_definitions())
31    val ths' = List.mapPartial prepare (current_theorems())
32    val axs' = List.mapPartial prepare (current_axioms())
33    val _ = List.app (ignore o export_thm) defs'
34    val _ = List.app (ignore o export_thm) ths'
35    val _ = List.app (ignore o export_thm) axs'
36    val _ = stop_logging()
37  in () end
38end
39