1.1 --- a/src/Tools/isac/Specify/calchead.sml	Thu May 07 12:15:37 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/calchead.sml	Thu May 07 14:11:03 2020 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4     --oris2fmz_vals--> ["equality (1+x=2)","boundVariable x","solutions L"] *)
     1.5  fun oris2fmz_vals oris =
     1.6    let fun ori2fmz_vals (_, _, _, dsc, ts) = 
     1.7 -	  ((UnparseC.term o I_Model.comp_dts') (dsc, ts), last_elem ts) 
     1.8 +	  ((UnparseC.term o O_Model.comp_dts') (dsc, ts), last_elem ts) 
     1.9  	  handle _ => error ("ori2fmz_env called with " ^ UnparseC.terms ts)
    1.10    in (split_list o (map ori2fmz_vals)) oris end
    1.11  
    1.12 @@ -208,7 +208,7 @@
    1.13    WN.11.03: + dont take first inter<>[]                       *)
    1.14  fun seek_oridts ctxt sel (d, ts) [] =
    1.15      ("seek_oridts: input ('" ^
    1.16 -        (UnparseC.term_in_ctxt ctxt (I_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
    1.17 +        (UnparseC.term_in_ctxt ctxt (O_Model.comp_dts (d, ts))) ^ "') not found in oris (typed)",
    1.18        (0, [], sel, d, ts),
    1.19        [])
    1.20    | seek_oridts ctxt sel (d, ts) ((id, vat, sel', d', ts') :: oris) =
    1.21 @@ -279,13 +279,13 @@
    1.22  
    1.23  (* get the first term in ts from ori *)
    1.24  fun getr_ct thy (_, _, fd, d, ts) =
    1.25 -  (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d,[hd ts]))
    1.26 +  (fd, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d,[hd ts]))
    1.27  
    1.28  (* get a term from ori, notyet input in itm.
    1.29     the term from ori is thrown back to a string in order to reuse
    1.30     machinery for immediate input by the user. *)
    1.31  fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
    1.32 -  (fd, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts))
    1.33 +  (fd, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d, subtract op = (I_Model.ts_in itm_) ts))
    1.34  
    1.35  (* in FE dsc, not dat: this is in itms ...*)
    1.36  fun is_untouched (_, _, false, _, I_Model.Inc ((_, []), _)) = true
    1.37 @@ -306,7 +306,7 @@
    1.38          case find_first (test_d d) itms of SOME _ => true | NONE => false
    1.39      in
    1.40        case filter_out (is_elem itms) pbt of
    1.41 -        (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o I_Model.comp_dts) (d, []))
    1.42 +        (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o O_Model.comp_dts) (d, []))
    1.43        | _ => NONE
    1.44      end
    1.45    | nxt_add thy oris _ itms =
    1.46 @@ -451,7 +451,7 @@
    1.47  
    1.48  fun test_types ctxt (d,ts) =
    1.49    let 
    1.50 -    val opt = (try I_Model.comp_dts) (d, ts)
    1.51 +    val opt = (try O_Model.comp_dts) (d, ts)
    1.52      val msg = case opt of 
    1.53        SOME _ => "" 
    1.54      | NONE => (UnparseC.term_in_ctxt ctxt d ^ " " ^
    1.55 @@ -465,7 +465,7 @@
    1.56    let
    1.57      val ots = (distinct o flat o (map #5)) ori
    1.58      val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
    1.59 -    val (d, ts) = I_Model.split_dts t
    1.60 +    val (d, ts) = O_Model.split_dts t
    1.61      val ids = map (fst o dest_Free) ((distinct o (flat o (map TermC.vars))) ts)
    1.62    in
    1.63      if (subtract op = oids ids) <> []
    1.64 @@ -504,7 +504,7 @@
    1.65          case TermC.parseNEW ctxt ct of
    1.66            NONE => Add (i, [], false, sel, I_Model.Syn ct)
    1.67          | SOME t =>
    1.68 -            let val (d, ts) = I_Model.split_dts t
    1.69 +            let val (d, ts) = O_Model.split_dts t
    1.70              in 
    1.71                if d = TermC.empty 
    1.72                then Add (i, [], false, sel, I_Model.Mis (Specify.dsc_unknown, hd ts)) 
    1.73 @@ -563,7 +563,7 @@
    1.74  fun mtc thy (str, (dsc, _)) (ty $ var) =
    1.75      ((Thm.global_cterm_of thy (dsc $ var);(*type check*)
    1.76        SOME (([1], str, dsc, (*[var]*)
    1.77 -	    I_Model.split_dts' (dsc, var))) (*:ori without leading #*))
    1.78 +	    O_Model.split_dts' (dsc, var))) (*:ori without leading #*))
    1.79        handle e as TYPE _ => 
    1.80  	      (tracing (dashs 70 ^ "\n"
    1.81  	        ^ "*** ERROR while creating the items for the model of the ->problem\n"
    1.82 @@ -602,7 +602,7 @@
    1.83  fun cpy_nam pbt oris (p as (field, (dsc, t))) =
    1.84    (if is_copy_named_generating p
    1.85     then (*WN051014 kept strange old code ...*)
    1.86 -     let fun sel (_,_,d,ts) = I_Model.comp_ts (d, ts) 
    1.87 +     let fun sel (_,_,d,ts) = O_Model.comp_ts (d, ts) 
    1.88         val cy' = (implode o (drop_last_n 3) o Symbol.explode o TermC.free2str) t
    1.89         val ext = (last_elem o drop_last o Symbol.explode o TermC.free2str) t
    1.90         val vars' = map (Term.term_name o snd o snd) pbt (*cpy-nam filtered_out*)
    1.91 @@ -624,7 +624,7 @@
    1.92      val cy = filter is_copy_named pbt  (* cy is NOT a (formal) argument, but the fun's result *)
    1.93      val oris' = matc thy pbt' ags []
    1.94      val cy' = map (cpy_nam pbt' oris') cy
    1.95 -    val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
    1.96 +    val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
    1.97    in (map flattup ors) end
    1.98  
    1.99  (* report part of the error-msg which is not available in match_args *)