1.1 --- a/src/Tools/isac/Specify/specification.sml	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4      I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
     1.5    val reset: Calc.T -> Calc.T
     1.6  
     1.7 -  val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
     1.8 +  val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * MethodC.id -> bool
     1.9    val is_complete: Calc.T -> bool
    1.10  
    1.11  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
    1.12 @@ -84,7 +84,7 @@
    1.13  fun complete its pre (dI, pI, mI) = 
    1.14    foldl and_ (true, map #3 (its: I_Model.T)) andalso 
    1.15    foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso 
    1.16 -  dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
    1.17 +  dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> MethodC.id_empty
    1.18  
    1.19  fun get_data (pt, (p, _)) =
    1.20    case Ctree.get_obj I pt p of
    1.21 @@ -119,7 +119,7 @@
    1.22  		  val (ospec, hdf', spec, meth) = case Ctree.get_obj I pt p of
    1.23  		    Ctree.PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
    1.24  		  | _ => raise ERROR "get Met: uncovered case get_obj"
    1.25 -      val {prls, pre, ...} = Method.from_store (#3 (References.select ospec spec))
    1.26 +      val {prls, pre, ...} = MethodC.from_store (#3 (References.select ospec spec))
    1.27        val (_, pre)  = Pre_Conds.check prls pre meth 0
    1.28      in
    1.29        (complete meth pre spec, Pos.Met, hdf', meth, pre, spec)