1.1 --- a/src/Tools/isac/Specify/o-model.sml	Sat Feb 04 11:21:56 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Sat Feb 04 16:20:45 2023 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4  \<^isac_test>\<open>
     1.5  fun preori2str (vs, fi, t, ts) = 
     1.6    "(" ^ (strs2str o (map string_of_int)) vs ^ ", " ^ fi ^ ", " ^
     1.7 -  UnparseC.term t ^ ", " ^ (strs2str o (map UnparseC.term)) ts ^ ")";
     1.8 +  UnparseC.term t ^ ", " ^ (strs2str o (map TermC.unparse_ERROR)) ts ^ ")";
     1.9  val string_of_preoris = (strs2str' o (map (linefeed o preori2str)));
    1.10  \<close>
    1.11  
    1.12 @@ -104,12 +104,12 @@
    1.13  (** initialise O_Model **)
    1.14  
    1.15  (* compare d and dsc in pbt and transfer field to where_-ori *)
    1.16 -fun add_field (_: theory) pbt (d,ts) = 
    1.17 +fun add_field thy pbt (d,ts) = 
    1.18    let fun eq d pt = (d = (fst o snd) pt);
    1.19    in case filter (eq d) pbt of
    1.20         [(fi, (_, _))] => (fi, d, ts)
    1.21       | [] => ("#undef", d, ts)   (*may come with met.model*)
    1.22 -     | _ => raise ERROR ("add_field: " ^ UnparseC.term d ^ " more than once in pbt")
    1.23 +     | _ => raise ERROR ("add_field: " ^ UnparseC.term_in_thy thy d ^ " more than once in pbt")
    1.24    end;
    1.25  
    1.26  (*
    1.27 @@ -266,7 +266,7 @@
    1.28      else ([1], field, dsc, [t])
    1.29  	\<close> of
    1.30      SOME x => x
    1.31 -  | NONE => raise ERROR ("copy_name: for "^ UnparseC.term t)
    1.32 +  | NONE => raise ERROR ("copy_name: for " ^ TermC.unparse_ERROR t)
    1.33  
    1.34  
    1.35  (** tools for I_Model **)