1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Thu Mar 15 14:50:29 2018 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Thu Mar 15 15:26:06 2018 +0100
     1.3 @@ -49,14 +49,14 @@
     1.4    val vals_of_oris : Model.ori list -> term list
     1.5    val is_error : Model.itm_ -> bool
     1.6    val is_copy_named : 'a * ('b * term) -> bool
     1.7 -  val ori2Coritm : pat list -> Model.ori -> Model.itm
     1.8 +  val ori2Coritm : Celem.pat list -> Model.ori -> Model.itm
     1.9    val is_copy_named_idstr : string -> bool
    1.10    val matc : theory -> (string * (term * term)) list -> term list -> Model.preori list -> Model.preori list
    1.11 -  val mtc : theory -> pat -> term -> Model.preori option
    1.12 -  val cpy_nam : pat list -> Model.preori list -> pat -> Model.preori
    1.13 +  val mtc : theory -> Celem.pat -> term -> Model.preori option
    1.14 +  val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori
    1.15    datatype additm = Add of Model.itm | Err of string
    1.16    val appl_add: Proof.context -> string -> (int * Model.vats * string * term * term list) list ->
    1.17 -    (int * ''a * ''b * string * Model.itm_) list -> (string * (term * term)) list -> cterm' -> additm
    1.18 +    (int * ''a * ''b * string * Model.itm_) list -> (string * (term * term)) list -> Celem.cterm' -> additm
    1.19  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.20  
    1.21  (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)

     2.1 --- a/src/Tools/isac/Interpret/ctree-access.sml	Thu Mar 15 14:50:29 2018 +0100
     2.2 +++ b/src/Tools/isac/Interpret/ctree-access.sml	Thu Mar 15 15:26:06 2018 +0100
     2.3 @@ -38,7 +38,7 @@
     2.4    val update_loc' : CTbasic.ctree -> CTbasic.pos ->
     2.5      (Selem.istate * Proof.context) option * (Selem.istate * Proof.context) option -> CTbasic.ctree
     2.6    val append_problem : int list -> Selem.istate * Proof.context -> Selem.fmz ->
     2.7 -    Model.ori list * spec * term -> CTbasic.ctree -> CTbasic.ctree
     2.8 +    Model.ori list * Celem.spec * term -> CTbasic.ctree -> CTbasic.ctree
     2.9  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.10  end
    2.11  (**)

     3.1 --- a/src/Tools/isac/Interpret/inform.sml	Thu Mar 15 14:50:29 2018 +0100
     3.2 +++ b/src/Tools/isac/Interpret/inform.sml	Thu Mar 15 15:26:06 2018 +0100
     3.3 @@ -19,18 +19,18 @@
     3.4  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     3.5    val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
     3.6    val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
     3.7 -  val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c)
     3.8 +  val rev_deriv' : 'a * Celem.rule * ('b * 'c) -> 'b * Celem.rule * ('a * 'c)
     3.9    val compare_step : Generate.taci list * Ctree.pos' list * (Ctree.state) -> term -> string * Chead.calcstate'
    3.10 -  val check_err_patt : term * term -> subst -> errpatID * term -> rls -> errpatID option
    3.11 +  val check_err_patt : term * term -> Celem.subst -> Celem.errpatID * term -> Celem.rls -> Celem.errpatID option
    3.12    val concat_deriv : 'a * ((term * term) list -> term * term -> bool) ->
    3.13 -    rls -> rule list -> term -> term -> bool * (term * rule * (term * term list)) list
    3.14 +    Celem.rls -> Celem.rule list -> term -> term -> bool * (term * Celem.rule * (term * term list)) list
    3.15    val check_error_patterns :
    3.16      term * term ->
    3.17 -    term * (term * term) list -> (errpatID * term list * 'a list) list * rls -> errpatID option
    3.18 +    term * (term * term) list -> (Celem.errpatID * term list * 'a list) list * Celem.rls -> Celem.errpatID option
    3.19    val get_fillform :
    3.20 -     'a * (term * term) list -> 'b * term -> errpatID -> fillpat -> (fillpatID * term * 'b * 'a) option
    3.21 +     'a * (term * term) list -> 'b * term -> Celem.errpatID -> Celem.fillpat -> (Celem.fillpatID * term * 'b * 'a) option
    3.22    val get_fillpats :
    3.23 -     'a * (term * term) list -> term -> errpatID -> thm -> (fillpatID * term * thm * 'a) list
    3.24 +     'a * (term * term) list -> term -> Celem.errpatID -> thm -> (Celem.fillpatID * term * thm * 'a) list
    3.25  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    3.26  
    3.27  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

     4.1 --- a/src/Tools/isac/Interpret/rewtools.sml	Thu Mar 15 14:50:29 2018 +0100
     4.2 +++ b/src/Tools/isac/Interpret/rewtools.sml	Thu Mar 15 15:26:06 2018 +0100
     4.3 @@ -46,9 +46,10 @@
     4.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     4.5    (*  NONE *)
     4.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     4.7 -  val trtas2str : (term * rule * (term * term list)) list -> string
     4.8 -  val eq_Thm : rule * rule -> bool
     4.9 -  val deriv2str : (term * rule * (term * term list)) list -> string val deriv_of_thm'' : thm'' -> string
    4.10 +  val trtas2str : (term * Celem.rule * (term * term list)) list -> string
    4.11 +  val eq_Thm : Celem.rule * Celem.rule -> bool
    4.12 +  val deriv2str : (term * Celem.rule * (term * term list)) list -> string
    4.13 +  val deriv_of_thm'' : Celem.thm'' -> string
    4.14  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    4.15  
    4.16  (*----- unused code, kept as hints to design ideas ---------------------------------------------*)

     5.1 --- a/src/Tools/isac/Interpret/script.sml	Thu Mar 15 14:50:29 2018 +0100
     5.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Mar 15 15:26:06 2018 +0100
     5.3 @@ -30,17 +30,18 @@
     5.4    datatype asap = Aundef | AssOnly | AssGen
     5.5    datatype appy = Appy of Tac.tac_ * Selem.scrstate | Napp of LTool.env | Skip of term * LTool.env
     5.6    datatype appy_ = Napp_ | Skip_
     5.7 -  val appy : theory' * rls -> Ctree.state -> LTool.env -> lrd list -> term -> term option -> term -> appy
     5.8 +  val appy : Celem.theory' * Celem.rls -> Ctree.state -> LTool.env -> Celem.lrd list -> term ->
     5.9 +    term option -> term -> appy
    5.10    val formal_args : term -> term list
    5.11    val get_stac : 'a -> term -> term option 
    5.12 -  val go : loc_ -> term -> term
    5.13 -  val handle_leaf : string -> theory' -> rls -> LTool.env -> term option -> term -> term -> 
    5.14 +  val go : Celem.loc_ -> term -> term
    5.15 +  val handle_leaf : string -> Celem.theory' -> Celem.rls -> LTool.env -> term option -> term -> term -> 
    5.16      term option * LTool.stacexpr
    5.17    val id_of_scr : term -> string
    5.18     val is_spec_pos : Ctree.pos_ -> bool
    5.19 -  val itms2args : 'a -> metID -> Model.itm list -> term list
    5.20 -  val nstep_up : theory' * rls -> Ctree.state -> scr -> LTool.env -> lrd list -> appy_ -> 
    5.21 -    term option -> term -> appy
    5.22 +  val itms2args : 'a -> Celem.metID -> Model.itm list -> term list
    5.23 +  val nstep_up : Celem.theory' * Celem.rls -> Ctree.state -> Celem.scr -> LTool.env ->
    5.24 +    Celem.lrd list -> appy_ -> term option -> term -> appy
    5.25    val stac2tac : Ctree.ctree -> theory -> term -> Tac.tac
    5.26    val stac2tac_ : Ctree.ctree -> theory -> term -> Tac.tac * Tac.tac_
    5.27    val upd_env_opt : LTool.env -> term option * term -> LTool.env

     6.1 --- a/src/Tools/isac/ProgLang/calculate.sml	Thu Mar 15 14:50:29 2018 +0100
     6.2 +++ b/src/Tools/isac/ProgLang/calculate.sml	Thu Mar 15 15:26:06 2018 +0100
     6.3 @@ -17,7 +17,7 @@
     6.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     6.5    (* NONE *)
     6.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     6.7 -    val get_pair: theory -> string -> eval_fn -> term -> (string * term) option
     6.8 +    val get_pair: theory -> string -> Celem.eval_fn -> term -> (string * term) option
     6.9      val mk_rule: term list * term * term -> term
    6.10      val divisors: int -> int list
    6.11      val doubles: int list -> int list

     7.1 --- a/src/Tools/isac/ProgLang/rewrite.sml	Thu Mar 15 14:50:29 2018 +0100
     7.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml	Thu Mar 15 15:26:06 2018 +0100
     7.3 @@ -24,10 +24,11 @@
     7.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     7.5    (* NONE *)
     7.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     7.7 -    val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) -> rls -> bool -> thm -> term -> (term * term list) option
     7.8 -    val rewrite__set_: theory -> int -> bool -> (term * term) list -> rls -> term -> (term * term list) option
     7.9 -    val app_rev: theory -> int -> rls -> term -> term * term list * bool
    7.10 -    val app_sub: theory -> int -> rls -> term -> term * term list * bool
    7.11 +    val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
    7.12 +      Celem.rls -> bool -> thm -> term -> (term * term list) option
    7.13 +    val rewrite__set_: theory -> int -> bool -> (term * term) list -> Celem.rls -> term -> (term * term list) option
    7.14 +    val app_rev: theory -> int -> Celem.rls -> term -> term * term list * bool
    7.15 +    val app_sub: theory -> int -> Celem.rls -> term -> term * term list * bool
    7.16      val mk_thm: theory -> string -> thm
    7.17      val trace1: int -> string -> unit
    7.18  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

     8.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Thu Mar 15 14:50:29 2018 +0100
     8.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Thu Mar 15 15:26:06 2018 +0100
     8.3 @@ -28,8 +28,8 @@
     8.4  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     8.5    (* NONE *)
     8.6  (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     8.7 -    val rule2stac: theory -> rule -> term
     8.8 -    val rule2stac_inst: theory -> rule -> term
     8.9 +    val rule2stac: theory -> Celem.rule -> term
    8.10 +    val rule2stac_inst: theory -> Celem.rule -> term
    8.11      val @@ : term list -> term
    8.12  ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    8.13    end

     9.1 --- a/src/Tools/isac/calcelems.sml	Thu Mar 15 14:50:29 2018 +0100
     9.2 +++ b/src/Tools/isac/calcelems.sml	Thu Mar 15 15:26:06 2018 +0100
     9.3 @@ -121,7 +121,7 @@
     9.4      val term_to_string': Proof.context -> term -> string
     9.5      val thy2ctxt': string -> Proof.context
     9.6      type rrlsstate = term * term * rule list list * (rule * (term * term list)) list
     9.7 -    type loc_ = lrd list
     9.8 +    type loc_ (*= lrd list*)
     9.9      val loc_2str: loc_ -> string
    9.10      val e_spec: spec
    9.11      val env2str: subst -> string