src/Tools/isac/Specify/m-match.sml
changeset 60653 fff1c0f0a9e7
parent 60650 06ec8abfd3bc
child 60655 f73460617c3d
     1.1 --- a/src/Tools/isac/Specify/m-match.sml	Wed Jan 25 17:51:52 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/m-match.sml	Wed Jan 25 18:35:02 2023 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4  (* match a formalization with a problem type, for tests *)
     1.5  fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) =
     1.6    let
     1.7 -    val oris = O_Model.init thy fmz model(* |> #1*);
     1.8 +    val (oris, _) = O_Model.init thy fmz model(* |> #1*);
     1.9      val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er);
    1.10    in
    1.11      if bool