src/Tools/isac/BaseDefinitions/model-pattern.sml
changeset 60675 d841c720d288
parent 60660 c4b24621077e
child 60688 ee663dd09aa1
     1.1 --- a/src/Tools/isac/BaseDefinitions/model-pattern.sml	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/src/Tools/isac/BaseDefinitions/model-pattern.sml	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4    let
     1.5      val (m_field, (hd, arg)) = case strip_comb dsc_tm of
     1.6        (hd, [arg]) => (m_field, (hd, arg))
     1.7 -    | _ => error ("Wrong descriptor " ^ quote (UnparseC.term_in_ctxt ctxt dsc_tm) ^ Position.here pos)
     1.8 +    | _ => error ("Wrong descriptor " ^ quote (UnparseC.term ctxt dsc_tm) ^ Position.here pos)
     1.9    in (m_field, (hd, arg), pos) end
    1.10  
    1.11  
    1.12 @@ -85,7 +85,7 @@
    1.13    in (model, where_) end
    1.14  
    1.15  fun pat2str ctxt (field, (dsc, id)) =
    1.16 -  pair2str (field, pair2str (UnparseC.term_in_ctxt ctxt dsc, UnparseC.term_in_ctxt ctxt id));
    1.17 +  pair2str (field, pair2str (UnparseC.term ctxt dsc, UnparseC.term ctxt id));
    1.18  fun to_string ctxt pats = (strs2str o (map (pat2str ctxt))) pats;
    1.19  
    1.20  \<^isac_test>\<open>