src/Tools/isac/Specify/p-spec.sml
changeset 60567 bb3140a02f3d
parent 60559 aba19e46dd84
child 60585 b7071d1dd263
     1.1 --- a/src/Tools/isac/Specify/p-spec.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/src/Tools/isac/Specify/p-spec.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4          => (fmz, fmz_, oris, ospec, hdf', sspec, sdI, spI, smI, probl, meth)
     1.5        | _ => raise ERROR "input_icalhd: uncovered case of get_obj I pt p"
     1.6        val ctxt = Proof_Context.init_global (ThyC.get_theory sdI)
     1.7 -    in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.str2term hdf)) 
     1.8 +    in if CAS_Cmd.is_from hdf fmz then the (CAS_Cmd.input (TermC.parse ctxt hdf)) 
     1.9         else        (*hacked WN0602 ~~~            ~~~~~~~~~,   ..dropped !*)
    1.10           let val (pos_, pits, mits) = 
    1.11  	         if dI <> sdI