1signature OpenTheoryCommon =
2sig
3
4val thy_tyop_to_string  : OpenTheoryMap.thy_tyop  -> string
5val thy_const_to_string : OpenTheoryMap.thy_const -> string
6
7datatype object
8= ONum of int
9| OName of string
10| OList of object list
11| OTypeOp of OpenTheoryMap.thy_tyop
12| OType of Type.hol_type
13| OConst of OpenTheoryMap.thy_const
14| OVar of Term.term
15| OTerm of Term.term
16| OThm of Thm.thm
17
18val object_compare : object * object -> order
19
20val tyvar_to_ot   : string -> OpenTheoryMap.otname
21val tyvar_from_ot : OpenTheoryMap.otname -> string
22end
23