1.1 --- a/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:02:06 2010 +0200
1.2 +++ b/src/Tools/isac/ME/calchead.sml Thu Aug 19 15:20:53 2010 +0200
1.3 @@ -16,7 +16,7 @@
1.4 val all_modspec : ptree * pos' -> ptree * pos'
1.5 datatype appl = Appl of tac_ | Notappl of string
1.6 val appl_add :
1.7 - Theory.theory ->
1.8 + theory ->
1.9 string ->
1.10 SpecifyTools.ori list ->
1.11 SpecifyTools.itm list ->
1.12 @@ -25,9 +25,9 @@
1.13 type calcstate'
1.14 val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
1.15 val chktyp :
1.16 - Theory.theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
1.17 + theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
1.18 val chktyps :
1.19 - Theory.theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
1.20 + theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
1.21 val complete_metitms :
1.22 SpecifyTools.ori list ->
1.23 SpecifyTools.itm list ->
1.24 @@ -49,7 +49,7 @@
1.25 'e * 'f * 'g * Term.term * 'h -> bool
1.26 val eq_dsc : SpecifyTools.itm * SpecifyTools.itm -> bool
1.27 val eq_pos' : ''a * pos_ -> ''a * pos_ -> bool
1.28 - val f_mout : Theory.theory -> mout -> Term.term
1.29 + val f_mout : theory -> mout -> Term.term
1.30 val filter_outs :
1.31 SpecifyTools.ori list ->
1.32 SpecifyTools.itm list -> SpecifyTools.ori list
1.33 @@ -71,13 +71,13 @@
1.34 val get_ocalhd : ptree * pos' -> ocalhd
1.35 val get_spec_form : tac_ -> pos' -> ptree -> mout
1.36 val geti_ct :
1.37 - Theory.theory ->
1.38 + theory ->
1.39 SpecifyTools.ori -> SpecifyTools.itm -> string * cterm'
1.40 - val getr_ct : Theory.theory -> SpecifyTools.ori -> string * cterm'
1.41 + val getr_ct : theory -> SpecifyTools.ori -> string * cterm'
1.42 val has_list_type : Term.term -> bool
1.43 val header : pos_ -> pblID -> metID -> pblmet
1.44 val insert_ppc :
1.45 - Theory.theory ->
1.46 + theory ->
1.47 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.48 SpecifyTools.itm list -> SpecifyTools.itm list
1.49 val insert_ppc' :
1.50 @@ -91,13 +91,13 @@
1.51 val is_error : SpecifyTools.itm_ -> bool
1.52 val is_field_correct : ''a -> ''b -> (''a * ''b list) list -> bool
1.53 val is_known :
1.54 - Theory.theory ->
1.55 + theory ->
1.56 string ->
1.57 SpecifyTools.ori list ->
1.58 Term.term -> string * SpecifyTools.ori * Term.term list
1.59 val is_list_type : Term.typ -> bool
1.60 val is_notyet_input :
1.61 - Theory.theory ->
1.62 + theory ->
1.63 SpecifyTools.itm list ->
1.64 Term.term list ->
1.65 SpecifyTools.ori ->
1.66 @@ -105,25 +105,25 @@
1.67 val is_parsed : SpecifyTools.itm_ -> bool
1.68 val is_untouched : SpecifyTools.itm -> bool
1.69 val matc :
1.70 - Theory.theory ->
1.71 + theory ->
1.72 pat list ->
1.73 Term.term list ->
1.74 (int list * string * Term.term * Term.term list) list ->
1.75 (int list * string * Term.term * Term.term list) list
1.76 val match_ags :
1.77 - Theory.theory -> pat list -> Term.term list -> SpecifyTools.ori list
1.78 + theory -> pat list -> Term.term list -> SpecifyTools.ori list
1.79 val maxl : int list -> int
1.80 val match_ags_msg : string list -> Term.term -> Term.term list -> unit
1.81 val memI : ''a list -> ''a -> bool
1.82 val mk_additem : string -> cterm' -> tac
1.83 - val mk_delete : Theory.theory -> string -> SpecifyTools.itm_ -> tac
1.84 + val mk_delete : theory -> string -> SpecifyTools.itm_ -> tac
1.85 val mtc :
1.86 - Theory.theory -> pat -> Term.term -> SpecifyTools.preori Library.option
1.87 + theory -> pat -> Term.term -> SpecifyTools.preori option
1.88 val nxt_add :
1.89 - Theory.theory ->
1.90 + theory ->
1.91 SpecifyTools.ori list ->
1.92 (string * (Term.term * 'a)) list ->
1.93 - SpecifyTools.itm list -> (string * cterm') Library.option
1.94 + SpecifyTools.itm list -> (string * cterm') option
1.95 val nxt_model_pbl : tac_ -> ptree * (int list * pos_) -> tac_
1.96 val nxt_spec :
1.97 pos_ ->
1.98 @@ -147,7 +147,7 @@
1.99 SpecifyTools.itm_ ->
1.100 Term.term -> Term.term list -> SpecifyTools.ori -> SpecifyTools.itm
1.101 val overwrite_ppc :
1.102 - Theory.theory ->
1.103 + theory ->
1.104 int * SpecifyTools.vats * bool * string * SpecifyTools.itm_ ->
1.105 SpecifyTools.itm list ->
1.106 (int * SpecifyTools.vats * bool * string * SpecifyTools.itm_) list
1.107 @@ -159,24 +159,24 @@
1.108 val ppc2list : 'a SpecifyTools.ppc -> 'a list
1.109 val pt_extract :
1.110 ptree * (int list * pos_) ->
1.111 - ptform * tac Library.option * Term.term list
1.112 + ptform * tac option * Term.term list
1.113 val pt_form : ppobj -> ptform
1.114 val pt_model : ppobj -> pos_ -> ptform
1.115 val reset_calchead : ptree * pos' -> ptree * pos'
1.116 val seek_oridts :
1.117 - Theory.theory ->
1.118 + theory ->
1.119 string ->
1.120 Term.term * Term.term list ->
1.121 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.122 -> string * SpecifyTools.ori * Term.term list
1.123 val seek_orits :
1.124 - Theory.theory ->
1.125 + theory ->
1.126 string ->
1.127 Term.term list ->
1.128 (int * SpecifyTools.vats * string * Term.term * Term.term list) list
1.129 -> string * SpecifyTools.ori * Term.term list
1.130 val seek_ppc :
1.131 - int -> SpecifyTools.itm list -> SpecifyTools.itm Library.option
1.132 + int -> SpecifyTools.itm list -> SpecifyTools.itm option
1.133 val show_pt : ptree -> unit
1.134 val some_spec : spec -> spec -> spec
1.135 val specify :
1.136 @@ -193,8 +193,8 @@
1.137 'b ->
1.138 ptree ->
1.139 (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
1.140 - val tag_form : Theory.theory -> Thm.cterm * Thm.cterm -> Thm.cterm
1.141 - val test_types : Theory.theory -> Term.term * Term.term list -> string
1.142 + val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
1.143 + val test_types : theory -> Term.term * Term.term list -> string
1.144 val typeless : Term.term -> Term.term
1.145 val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
1.146 val vals_of_oris : SpecifyTools.ori list -> Term.term list