1.1 --- a/src/Tools/isac/Specify/o-model.sml	Tue Apr 27 19:52:29 2021 +0200
     1.2 +++ b/src/Tools/isac/Specify/o-model.sml	Wed Apr 28 12:38:13 2021 +0200
     1.3 @@ -252,25 +252,30 @@
     1.4     e.g. (v_v, x) & (v_v'i', ?) --> (v_v'i', x_i),
     1.5     but leave is_copy_named_generating as is, e.t. ss''' *)
     1.6  fun cpy_nam pbt oris (p as (field, (dsc, t))) =
     1.7 -  (if is_copy_named_generating p
     1.8 -   then (*WN051014 kept strange old code ...*)
     1.9 -     let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts) 
    1.10 -       val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
    1.11 -       val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
    1.12 -       val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
    1.13 -       val vals = map sel oris
    1.14 -       val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
    1.15 -     in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
    1.16 -   else ([1], field, dsc, [t])
    1.17 -	) handle _ => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
    1.18 +  case \<^try>\<open>
    1.19 +    if is_copy_named_generating p
    1.20 +    then (*WN051014 kept strange old code ...*)
    1.21 +      let fun sel (_,_,d,ts) = Input_Descript.join'''' (d, ts) 
    1.22 +        val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
    1.23 +        val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
    1.24 +        val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
    1.25 +        val vals = map sel oris
    1.26 +        val cy_ext = (Term.term_name o the) (assoc (vars' ~~ vals, cy')) ^ "_" ^ ext
    1.27 +      in ([1], field, dsc, [TermC.mk_free (type_of t) cy_ext]) end
    1.28 +    else ([1], field, dsc, [t])
    1.29 +	\<close> of
    1.30 +    SOME x => x
    1.31 +  | NONE => raise ERROR ("cpy_nam: for "^ UnparseC.term t)
    1.32  
    1.33  (* ["BOOL (1+x=2)", "REAL x"] --match_ags--> oris 
    1.34     --values'--> ["equality (1+x=2)", "boundVariable x", "solutions L"] *)
    1.35  (*TODO: unify with values*)
    1.36  fun values' oris =
    1.37 -  let fun ori2fmz_vals (_, _, _, dsc, ts) = 
    1.38 -	  ((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts) 
    1.39 -	  handle _ => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
    1.40 +  let
    1.41 +    fun ori2fmz_vals (_, _, _, dsc, ts) = 
    1.42 +      case \<^try>\<open>((UnparseC.term o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
    1.43 +        SOME x => x
    1.44 +      | NONE => raise ERROR ("ori2fmz_env called with " ^ UnparseC.terms ts)
    1.45    in (split_list o (map ori2fmz_vals)) oris end
    1.46  
    1.47