src/Tools/isac/Specify/o-model.sml
changeset 59957 d63363c45af6
parent 59955 b24adc7c9875
child 59960 d0637de46bfa
     1.1 --- a/src/Tools/isac/Specify/o-model.sml	Sat May 09 15:31:15 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sun May 10 13:16:56 2020 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    type m_field = Model_Def.m_field
     1.5    type descriptor = Model_Def.descriptor
     1.6    val to_string: T -> string
     1.7 +  val single_to_string: single -> string
     1.8    val single_empty: single
     1.9  
    1.10    val init: Formalise.model -> theory -> Model_Pattern.T -> T
    1.11 @@ -46,6 +47,7 @@
    1.12  type T = Model_Def.o_model;
    1.13  type single = Model_Def.o_model_single
    1.14  val single_empty = Model_Def.o_model_empty;
    1.15 +val single_to_string = Model_Def.o_model_single_to_string;
    1.16  val to_string = Model_Def.o_model_to_string;
    1.17  
    1.18  (* O_Model.single without leading integer *)