1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Mon Jun 20 11:55:55 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Mon Jun 20 18:37:54 2022 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4      val thy = ThyC.get_theory dI
     1.5  	  val {ppc, ...} = Problem.from_store pI
     1.6  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
     1.7 -	  val its = O_Model.add_id its_
     1.8 +	  val its = O_Model.add_enumerate its_
     1.9  	  val pits = map flattup2 its
    1.10  	  val (pI, mI) =
    1.11        if mI <> ["no_met"]
    1.12 @@ -55,7 +55,7 @@
    1.13  			  | NONE => (pI, (hd o #met o Problem.from_store) pI)
    1.14  	  val {ppc, pre, prls, ...} = MethodC.from_store mI
    1.15  	  val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*)
    1.16 -	  val its = O_Model.add_id its_
    1.17 +	  val its = O_Model.add_enumerate its_
    1.18  	  val mits = map flattup2 its
    1.19  	  val (_, pre) = Pre_Conds.check prls pre mits 0
    1.20      val ctxt = Proof_Context.init_global thy