src/Tools/isac/Specify/i-model.sml
changeset 60691 057bee6fbe34
parent 60690 b7f19579bc25
child 60692 2cdf973fcaab
     1.1 --- a/src/Tools/isac/Specify/i-model.sml	Sun Feb 19 10:29:58 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/i-model.sml	Sun Feb 19 13:03:54 2023 +0100
     1.3 @@ -25,6 +25,7 @@
     1.4    val to_string: Proof.context -> T -> string
     1.5  
     1.6    datatype add_single = Add of single | Err of string
     1.7 +(*val init: Proof.context -> Model_Pattern.T -> T*)
     1.8    val init: Model_Pattern.T -> T
     1.9    val init_TEST: Proof.context -> Model_Pattern.T -> T
    1.10    val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
    1.11 @@ -119,7 +120,9 @@
    1.12      fun pat_to_item (m_field, (descriptor, _)) =
    1.13        (0, [], false, m_field, Syn (UnparseC.term ctxt descriptor ^ " " ^ empty_for (type_of descriptor)))
    1.14    in map pat_to_item model_patt end
    1.15 -
    1.16 +(*########################* )
    1.17 +val init = init_TEST
    1.18 +( *########################*)
    1.19  
    1.20  (** check input on a model **)
    1.21