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