1.1 --- a/src/Tools/isac/Specify/specification.sml	Mon May 18 14:02:54 2020 +0200
     1.2 +++ b/src/Tools/isac/Specify/specification.sml	Mon May 18 14:05:46 2020 +0200
     1.3 @@ -69,10 +69,6 @@
     1.4    val get_data: Calc.T ->
     1.5      I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context
     1.6  
     1.7 -(*/----- delete -----\* )
     1.8 -  val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T
     1.9 -( *\----- delete -----/*)
    1.10 -
    1.11  (*val ocalhd_complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool*)
    1.12    val complete: I_Model.T -> Pre_Conds.T -> ThyC.id * Problem.id * Method.id -> bool
    1.13  (*val is_complete_mod: Calc.T -> bool*)
    1.14 @@ -97,26 +93,6 @@
    1.15    foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso 
    1.16    dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty
    1.17  
    1.18 -(*/----- delete -----\* )
    1.19 -fun is_parsed (I_Model.Syn _) = false
    1.20 -  | is_parsed _ = true
    1.21 -
    1.22 -(* get a term from ori, notyet input in itm.
    1.23 -   the term from ori is thrown back to a string in order to reuse
    1.24 -   machinery for immediate input by the user. *)
    1.25 -fun geti_ct thy (_, _, _, d, ts) (_, _, _, fd, itm_) =
    1.26 -  (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, subtract op = (I_Model.ts_in itm_) ts))
    1.27 -( *\----- delete -----/*)
    1.28 -
    1.29 -(*/----- delete -----\* )
    1.30 -(* output the headline to a ppc *)
    1.31 -fun header p_ pI mI =
    1.32 -  case p_ of
    1.33 -    Pos.Pbl => Test_Out.Problem (if pI = Problem.id_empty then [] else pI) 
    1.34 -	| Pos.Met => Test_Out.Method mI
    1.35 -	| pos => raise ERROR ("header called with "^ Pos.pos_2str pos)
    1.36 -( *\----- delete -----/*)
    1.37 -
    1.38  (** )
    1.39  fun make m_field (term_as_string, i_model) =
    1.40    case m_field of
    1.41 @@ -132,19 +108,6 @@
    1.42        => (meth, oris, (dI', pI', mI'), probl, (dI, pI, mI), ctxt)
    1.43    | _ => raise ERROR "specify_additem: uncovered case of get_obj I pt p";
    1.44  
    1.45 -
    1.46 -(*/----- delete -----\* )
    1.47 -(* fun tag_form thy (formal, given) = Thm.global_cterm_of thy
    1.48 -	 (((head_of o Thm.term_of) given) $ (Thm.term_of formal)); WN100819 *)
    1.49 -fun tag_form thy (formal, given) =
    1.50 - (let
    1.51 -    val gf = (head_of given) $ formal;
    1.52 -    val _ = Thm.global_cterm_of thy gf
    1.53 -  in gf end)
    1.54 -  handle _ => raise ERROR ("calchead.tag_form: " ^ UnparseC.term_in_thy thy given ^
    1.55 -    " .. " ^ UnparseC.term_in_thy thy formal ^ " ..types do not match")
    1.56 -( *\----- delete -----/*)
    1.57 -
    1.58  fun is_complete (pt, pos as (p, Pos.Pbl)) =
    1.59      if (Ctree.is_pblobj o (Ctree.get_obj I pt)) p 
    1.60      then (I_Model.is_complete o (Ctree.get_obj Ctree.g_pbl pt)) p
    1.61 @@ -156,23 +119,6 @@
    1.62    | is_complete (_, pos) =
    1.63      raise ERROR ("is_complete called by " ^ Pos.pos'2str pos ^ " (should be Pbl or Met)")
    1.64  
    1.65 -(*/----- delete -----\* )
    1.66 -(** get the formula from a ctree-node **)
    1.67 -(*
    1.68 -  take form+res from PblObj and 1.PrfObj and (PrfObj after PblObj)
    1.69 -  take res from all other PrfObj's
    1.70 -  Designed for interSteps, outcommented 04 in favour of calcChangedEvent
    1.71 -*)
    1.72 -fun formres p (Ctree.Nd (Ctree.PblObj {origin = (_, _, h), result = (r, _), ...}, _)) =
    1.73 -    [("headline", (p, Pos.Frm), h), ("stepform", (p, Pos.Res), r)]
    1.74 -  | formres p (Ctree.Nd (Ctree.PrfObj {form, result = (r, _), ...}, _)) = 
    1.75 -    [("stepform", (p, Pos.Frm), form), ("stepform", (p, Pos.Res), r)]
    1.76 -  | formres _ _ = raise ERROR "formres: uncovered definition" 
    1.77 -fun form p (Ctree.Nd (Ctree.PrfObj {result = (r, _), ...}, _)) = 
    1.78 -    [("stepform", (p, Pos.Res), r)]
    1.79 -  | form _ _ = raise ERROR "form: uncovered definition" 
    1.80 -( *\----- delete -----/*)
    1.81 -
    1.82  (* get a calchead from a PblObj-node in the ctree; preconditions must be calculated *)
    1.83  fun get (pt, (p, Pos.Pbl)) = 
    1.84      let