1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Mon Jan 30 09:47:18 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Mon Jan 30 12:11:40 2023 +0100
     1.3 @@ -104,7 +104,9 @@
     1.4        Parse.!!! (Parse.ML_source -- parse_theory -- parse_problem -- parse_method))
     1.5        >> (fn (term, (((source, thry), pbl), met)) => Toplevel.theory (fn thy =>
     1.6          let
     1.7 -          val t = TermC.parse (Proof_Context.init_global thy) term;
     1.8 +        (*/------------ replace by ParseC.term_position ------------------\*)
     1.9 +          val SOME t = ParseC.term_opt (Proof_Context.init_global thy) term;
    1.10 +        (*\------------ replace by ParseC.term_position ------------------/*)
    1.11            val pblID = References_Def.explode_id pbl;
    1.12            val metID = References_Def.explode_id met;
    1.13            val set_data =