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