1.1 --- a/src/Tools/isac/MathEngBasic/mstools.sml	Tue Apr 21 12:26:08 2020 +0200
     1.2 +++ b/src/Tools/isac/MathEngBasic/mstools.sml	Tue Apr 21 15:42:50 2020 +0200
     1.3 @@ -12,20 +12,20 @@
     1.4    val check_preconds : 'a -> Rule_Set.T -> term list -> Model.itm list -> (bool * term) list
     1.5    val check_preconds' : Rule_Set.T -> term list -> Model.itm list -> 'a -> (bool * term) list
     1.6  
     1.7 -  datatype match_ = Match_ of Celem.pblID * (Model.itm list * (bool * term) list) | NoMatch_
     1.8 +  datatype match_ = Match_ of Spec.pblID * (Model.itm list * (bool * term) list) | NoMatch_
     1.9    val refined_ : match_ list -> match_ option
    1.10 -  datatype match = Matches of Celem.pblID * Model.item Model.ppc | NoMatch of Celem.pblID * Model.item Model.ppc
    1.11 +  datatype match = Matches of Spec.pblID * Model.item Model.ppc | NoMatch of Spec.pblID * Model.item Model.ppc
    1.12    val matchs2str : match list -> string
    1.13    val common_subthy : theory * theory -> theory
    1.14  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.15    val pres2str : (bool * term) list -> string
    1.16 -  val refined : match list -> Celem.pblID
    1.17 +  val refined : match list -> Spec.pblID
    1.18  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.19    (*NONE*)
    1.20  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.21  
    1.22  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
    1.23 -  val pblID_of_match : match -> Celem.pblID
    1.24 +  val pblID_of_match : match -> Spec.pblID
    1.25    val refined_IDitms : match list -> match option
    1.26  end
    1.27  
    1.28 @@ -33,8 +33,8 @@
    1.29  struct
    1.30  
    1.31  datatype match = 
    1.32 -  Matches of Celem.pblID *  Model.item Model.ppc
    1.33 -| NoMatch of Celem.pblID *  Model.item  Model.ppc;
    1.34 +  Matches of Spec.pblID *  Model.item Model.ppc
    1.35 +| NoMatch of Spec.pblID *  Model.item  Model.ppc;
    1.36  fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^  Model.itemppc2str ppc ^ ")"
    1.37    | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^  Model.itemppc2str ppc ^ ")";
    1.38  fun matchs2str ms = (strs2str o (map match2str)) ms;
    1.39 @@ -43,7 +43,7 @@
    1.40  
    1.41  (* 10.03 for Refine_Problem *)
    1.42  datatype match_ = 
    1.43 -  Match_ of Celem.pblID * (( Model.itm list) * ((bool * term) list))
    1.44 +  Match_ of Spec.pblID * (( Model.itm list) * ((bool * term) list))
    1.45  | NoMatch_;
    1.46  
    1.47  (* the refined pbt is the last_element Matches in the list *)