1.1 --- a/src/Tools/isac/Specify/o-model.sml	Mon May 18 14:21:41 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Tue May 19 12:33:35 2020 +0200
     1.3 @@ -21,7 +21,6 @@
     1.4    val init: Formalise.model -> theory -> Model_Pattern.T -> T
     1.5    val add : theory -> Model_Pattern.T -> T -> T
     1.6    val values : T -> term list
     1.7 -(*val oris2fmz_vals: T -> string list * term list*)
     1.8    val values': T -> Formalise.model * term list
     1.9  
    1.10  (*/------- rename -------\*)
    1.11 @@ -45,6 +44,7 @@
    1.12    val coll_variants: ('a * ''b) list -> ('a list * ''b) list
    1.13    val replace_0: int -> int list -> int list
    1.14    val flattup: 'a * ('b * ('c * 'd * 'e)) -> 'a * 'b * 'c * 'd * 'e
    1.15 + val mark: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
    1.16  (*\------- rename -------/*)
    1.17  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.18  end
    1.19 @@ -143,11 +143,12 @@
    1.20  fun init [] _ _ = []
    1.21    | init fmz thy pbt =
    1.22      let
    1.23 -      val model = (map (fn str => str
    1.24 -                     |> TermC.parseNEW'' thy
    1.25 -                     |> Input_Descript.split
    1.26 -                     |> add_field thy pbt) fmz)
    1.27 -                  |> add_variants;
    1.28 +      val model =
    1.29 +        (map (fn str => str
    1.30 +          |> TermC.parseNEW'' thy
    1.31 +          |> Input_Descript.split
    1.32 +          |> add_field thy pbt) fmz)
    1.33 +        |> add_variants;
    1.34        val maxv = model |> map fst |> max;
    1.35        val maxv = if maxv = 0 then 1 else maxv;
    1.36        val model' = model