1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Mon Nov 02 15:16:07 2020 +0100
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Wed Nov 04 09:59:30 2020 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    type imodel = iitem list
     1.5    type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * References.T
     1.6    val empty: icalhd
     1.7 -  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Specification.T
     1.8 +  val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * SpecificationC.T
     1.9  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.10    (*  NONE *)
    1.11  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
    1.12 @@ -235,12 +235,12 @@
    1.13  	          then let val {prls,where_,...} = Problem.from_store (#2 (References.select ospec spec))
    1.14  		               val (_, pre) = Pre_Conds.check prls where_ pits 0
    1.15  	               in (Ctree.update_pbl pt p pits,
    1.16 -		                 (Specification.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): Specification.T) 
    1.17 +		                 (SpecificationC.complete pits pre spec, Pos.Pbl, hdf', pits, pre, spec): SpecificationC.T) 
    1.18                   end
    1.19  	           else let val {prls,pre,...} = Method.from_store (#3 (References.select ospec spec))
    1.20  		                val (_, pre) = Pre_Conds.check prls pre mits 0
    1.21  	                in (Ctree.update_met pt p mits,
    1.22 -		                  (Specification.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : Specification.T)
    1.23 +		                  (SpecificationC.complete mits pre spec, Pos.Met, hdf', mits, pre, spec) : SpecificationC.T)
    1.24                    end
    1.25           end 
    1.26      end