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