src/Tools/isac/Specify/o-model.sml
changeset 60734 a3aaca90af25
parent 60678 4b5be1a53e17
child 60760 3b173806efe2
     1.1 --- a/src/Tools/isac/Specify/o-model.sml	Fri Aug 18 18:51:18 2023 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sat Aug 19 05:06:55 2023 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4    val add_field: theory -> Model_Pattern.T -> descriptor * values -> m_field * descriptor * values
     1.5  
     1.6    val add_variants: ('a * ''b * 'c) list -> (int * ('a * ''b * 'c)) list
     1.7 -  val max_variant: variants -> int
     1.8 +  val get_max_variant: variants -> variant
     1.9    val partition_variants: ('a * 'a -> bool) -> 'a list -> (int * 'a) list
    1.10    val collect_variants: ('a * ''b) list -> ('a list * ''b) list
    1.11  
    1.12 @@ -137,8 +137,8 @@
    1.13      fun eq (a, b) = curry op= (snd3 a) (snd3 b);
    1.14    in partition_variants eq fdts end;
    1.15  
    1.16 -fun max_variant [] = raise ERROR "max_variant of []"
    1.17 -  | max_variant (y :: ys) =
    1.18 +fun get_max_variant [] = raise ERROR "get_max_variant of []"
    1.19 +  | get_max_variant (y :: ys) =
    1.20    let fun mx x [] = x
    1.21  	| mx x (y :: ys) = if x < y then mx y ys else mx x ys;
    1.22  in mx y ys end;
    1.23 @@ -173,7 +173,7 @@
    1.24            |> Input_Descript.split
    1.25            |> add_field thy pbt) ts)
    1.26          |> add_variants;
    1.27 -      val maxv = model |> map fst |> max_variant;
    1.28 +      val maxv = model |> map fst |> get_max_variant;
    1.29        val maxv = if maxv = 0 then 1 else maxv;
    1.30        val model' = model
    1.31          |> collect_variants