1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Fri Oct 07 20:46:48 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Sat Oct 08 11:40:48 2022 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    let
     1.5      val thy = ThyC.get_theory dI
     1.6      val ctxt = Proof_Context.init_global thy
     1.7 -	  val {ppc, ...} = Problem.from_store_PIDE ctxt pI
     1.8 +	  val {ppc, ...} = Problem.from_store ctxt pI
     1.9  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.10  	  val its = O_Model.add_enumerate its_
    1.11  	  val pits = map flattup2 its
    1.12 @@ -52,9 +52,9 @@
    1.13        then (pI, mI)
    1.14  		  else
    1.15          case Refine.problem thy pI pits of
    1.16 -			    SOME (pI,_) => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
    1.17 -			  | NONE => (pI, (hd o #met o Problem.from_store_PIDE ctxt) pI)
    1.18 -	  val {ppc, pre, prls, ...} = MethodC.from_store_PIDE ctxt mI
    1.19 +			    SOME (pI,_) => (pI, (hd o #met o Problem.from_store ctxt) pI)
    1.20 +			  | NONE => (pI, (hd o #met o Problem.from_store ctxt) pI)
    1.21 +	  val {ppc, pre, prls, ...} = MethodC.from_store ctxt mI
    1.22  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.23  	  val its = O_Model.add_enumerate its_
    1.24  	  val mits = map flattup2 its
    1.25 @@ -102,7 +102,7 @@
    1.26        Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
    1.27        >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
    1.28          let
    1.29 -          val t = TermC.parse_strict(*parse_strict_PIDE*) thy term;
    1.30 +          val t = TermC.parse_strict thy term;
    1.31            val pblID = References_Def.explode_id pbl;
    1.32            val metID = References_Def.explode_id met;
    1.33            val set_data =