1.1 --- a/src/Tools/isac/Specify/refine.sml	Mon Jun 20 11:55:55 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/refine.sml	Mon Jun 20 18:37:54 2022 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4      let
     1.5        val _ = (tracing o (curry op ^ "*** pass ") o strs2str) (pblRD @ [pI])
     1.6        val {thy, ppc, where_, prls, ...} = py 
     1.7 -      val oris = O_Model.init fmz thy ppc(* |> #1*);
     1.8 +      val oris = O_Model.init thy fmz ppc(* |> #1*);
     1.9        (* WN020803: itms!: oris might _not_ be complete here *)
    1.10        val (b, (itms, pre')) = M_Match.match_oris' thy oris (ppc, where_, prls)
    1.11      in
    1.12 @@ -168,7 +168,7 @@
    1.13      let
    1.14        val _ = (tracing o ((curry op ^)"*** pass ") o strs2str) (pblRD @ [pI])
    1.15        val {thy, ppc, where_, prls, ...} = py 
    1.16 -      val oris = O_Model.init fmz thy ppc(* |> #1*);
    1.17 +      val oris = O_Model.init thy fmz ppc(* |> #1*);
    1.18        (* WN020803: itms!: oris might _not_ be complete here *)
    1.19        val(b, (itms, pre')) = M_Match.match_oris' thy oris (ppc,where_,prls);
    1.20      in