src/Tools/isac/Specify/cas-command.sml
changeset 60574 3860f08122d8
parent 60559 aba19e46dd84
child 60585 b7071d1dd263
     1.1 --- a/src/Tools/isac/Specify/cas-command.sml	Thu Oct 20 12:12:18 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/cas-command.sml	Fri Oct 21 15:19:00 2022 +0200
     1.3 @@ -102,7 +102,7 @@
     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_strict thy term;
     1.8 +          val t = TermC.parse (Proof_Context.init_global thy) term;
     1.9            val pblID = References_Def.explode_id pbl;
    1.10            val metID = References_Def.explode_id met;
    1.11            val set_data =