1.1 --- a/src/Tools/isac/Specify/Input_Descript.thy	Sat Feb 04 11:21:56 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/Input_Descript.thy	Sat Feb 04 16:20:45 2023 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4    | join (d, ts) = 
     1.5      case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
     1.6        SOME x => x
     1.7 -    | NONE => raise ERROR ("join: " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
     1.8 +    | NONE => raise ERROR ("join: " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
     1.9  fun join' (d, []) = 
    1.10      if for_real_list d
    1.11      then (d $ e_listReal)
    1.12 @@ -207,7 +207,7 @@
    1.13    | join' (d, ts) = 
    1.14      case \<^try>\<open> d $ (join'''' (d, ts))\<close> of
    1.15        SOME x => x
    1.16 -    | NONE => raise ERROR ("join': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
    1.17 +    | NONE => raise ERROR ("join': " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
    1.18  fun join''' (d, []) = 
    1.19      if for_real_list d
    1.20      then UnparseC.term (d $ e_listReal)
    1.21 @@ -217,7 +217,7 @@
    1.22    | join''' (d, ts) = 
    1.23      case \<^try>\<open> UnparseC.term (d $ (join'''' (d, ts)))\<close> of
    1.24        SOME x => x
    1.25 -    | NONE => raise ERROR ("join''': " ^ UnparseC.term d ^ " $ " ^ UnparseC.term (hd ts)); 
    1.26 +    | NONE => raise ERROR ("join''': " ^ TermC.unparse_ERROR d ^ " $ " ^ TermC.unparse_ERROR (hd ts)); 
    1.27  
    1.28  (**)end(**)
    1.29  \<close> ML \<open>