1.1 --- a/src/Pure/pure_thy.ML Fri Jun 17 18:33:25 2005 +0200
1.2 +++ b/src/Pure/pure_thy.ML Fri Jun 17 18:33:26 2005 +0200
1.3 @@ -2,7 +2,7 @@
1.4 ID: $Id$
1.5 Author: Markus Wenzel, TU Muenchen
1.6
1.7 -Theorem database, derived theory operations, and the ProtoPure theory.
1.8 +Theorem storage. The ProtoPure theory.
1.9 *)
1.10
1.11 signature BASIC_PURE_THY =
1.12 @@ -25,12 +25,12 @@
1.13 include BASIC_PURE_THY
1.14 datatype interval = FromTo of int * int | From of int | Single of int
1.15 val string_of_thmref: thmref -> string
1.16 + val theorem_space: theory -> NameSpace.T
1.17 val get_thm_closure: theory -> thmref -> thm
1.18 val get_thms_closure: theory -> thmref -> thm list
1.19 val single_thm: string -> thm list -> thm
1.20 val select_thm: thmref -> thm list -> thm list
1.21 val selections: string * thm list -> (thmref * thm) list
1.22 - val extern_thm_sg: Sign.sg -> string -> xstring
1.23 val fact_index_of: theory -> FactIndex.T
1.24 val valid_thms: theory -> thmref * thm list -> bool
1.25 val thms_containing: theory -> FactIndex.spec -> (string * thm list) list
1.26 @@ -47,31 +47,27 @@
1.27 val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
1.28 -> theory * thm list list
1.29 val note_thmss: theory attribute -> ((bstring * theory attribute list) *
1.30 - (thmref * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
1.31 + (thmref * theory attribute list) list) list ->
1.32 + theory -> theory * (bstring * thm list) list
1.33 val note_thmss_i: theory attribute -> ((bstring * theory attribute list) *
1.34 - (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
1.35 - val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
1.36 - val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
1.37 - val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory
1.38 - -> theory * thm list list
1.39 - val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory
1.40 - -> theory * thm list list
1.41 - val add_defs: bool -> ((bstring * string) * theory attribute list) list
1.42 - -> theory -> theory * thm list
1.43 - val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
1.44 - -> theory -> theory * thm list
1.45 - val add_defss: bool -> ((bstring * string list) * theory attribute list) list
1.46 - -> theory -> theory * thm list list
1.47 - val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list
1.48 - -> theory -> theory * thm list list
1.49 - val get_name: theory -> string
1.50 - val put_name: string -> theory -> theory
1.51 - val global_path: theory -> theory
1.52 - val local_path: theory -> theory
1.53 - val begin_theory: string -> theory list -> theory
1.54 - val end_theory: theory -> theory
1.55 - val checkpoint: theory -> theory
1.56 - val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
1.57 + (thm list * theory attribute list) list) list ->
1.58 + theory -> theory * (bstring * thm list) list
1.59 + val add_axioms: ((bstring * string) * theory attribute list) list ->
1.60 + theory -> theory * thm list
1.61 + val add_axioms_i: ((bstring * term) * theory attribute list) list ->
1.62 + theory -> theory * thm list
1.63 + val add_axiomss: ((bstring * string list) * theory attribute list) list ->
1.64 + theory -> theory * thm list list
1.65 + val add_axiomss_i: ((bstring * term list) * theory attribute list) list ->
1.66 + theory -> theory * thm list list
1.67 + val add_defs: bool -> ((bstring * string) * theory attribute list) list ->
1.68 + theory -> theory * thm list
1.69 + val add_defs_i: bool -> ((bstring * term) * theory attribute list) list ->
1.70 + theory -> theory * thm list
1.71 + val add_defss: bool -> ((bstring * string list) * theory attribute list) list ->
1.72 + theory -> theory * thm list list
1.73 + val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
1.74 + theory -> theory * thm list list
1.75 end;
1.76
1.77 structure PureThy: PURE_THY =
1.78 @@ -80,53 +76,46 @@
1.79
1.80 (*** theorem database ***)
1.81
1.82 -(** data kind 'Pure/theorems' **)
1.83 +(** dataype theorems **)
1.84
1.85 -structure TheoremsDataArgs =
1.86 -struct
1.87 +fun pretty_theorems thy theorems =
1.88 + let
1.89 + val prt_thm = Display.pretty_thm_sg thy;
1.90 + fun prt_thms (name, [th]) =
1.91 + Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
1.92 + | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
1.93 + val thmss = NameSpace.extern_table theorems;
1.94 + in Pretty.big_list "theorems:" (map prt_thms thmss) end;
1.95 +
1.96 +structure TheoremsData = TheoryDataFun
1.97 +(struct
1.98 val name = "Pure/theorems";
1.99 -
1.100 type T =
1.101 - {theorems: thm list NameSpace.table,
1.102 - index: FactIndex.T} ref;
1.103 + {theorems: thm list NameSpace.table,
1.104 + index: FactIndex.T} ref;
1.105
1.106 fun mk_empty _ =
1.107 ref {theorems = NameSpace.empty_table, index = FactIndex.empty}: T;
1.108
1.109 val empty = mk_empty ();
1.110 fun copy (ref x) = ref x;
1.111 - val prep_ext = mk_empty;
1.112 - val merge = mk_empty;
1.113 + val extend = mk_empty;
1.114 + fun merge _ = mk_empty;
1.115 + fun print thy (ref {theorems, index}) = Pretty.writeln (pretty_theorems thy theorems);
1.116 +end);
1.117
1.118 - fun pretty sg (ref {theorems, index = _}) =
1.119 - let
1.120 - val prt_thm = Display.pretty_thm_sg sg;
1.121 - fun prt_thms (name, [th]) =
1.122 - Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
1.123 - | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
1.124 -
1.125 - val thmss = NameSpace.extern_table theorems;
1.126 - in Pretty.big_list "theorems:" (map prt_thms thmss) end;
1.127 -
1.128 - fun print sg data = Pretty.writeln (pretty sg data);
1.129 -end;
1.130 -
1.131 -structure TheoremsData = TheoryDataFun(TheoremsDataArgs);
1.132 -val get_theorems_sg = TheoremsData.get_sg;
1.133 val get_theorems = TheoremsData.get;
1.134 -
1.135 -val extern_thm_sg = NameSpace.extern o #1 o #theorems o ! o get_theorems_sg;
1.136 +val theorem_space = #1 o #theorems o ! o get_theorems;
1.137 val fact_index_of = #index o ! o get_theorems;
1.138
1.139
1.140 -
1.141 (* print theory *)
1.142
1.143 val print_theorems = TheoremsData.print;
1.144
1.145 fun print_theory thy =
1.146 Display.pretty_full_theory thy @
1.147 - [TheoremsDataArgs.pretty (Theory.sign_of thy) (get_theorems thy)]
1.148 + [pretty_theorems thy (#theorems (! (get_theorems thy)))]
1.149 |> Pretty.chunks |> Pretty.writeln;
1.150
1.151
1.152 @@ -192,33 +181,32 @@
1.153
1.154 fun lookup_thms thy =
1.155 let
1.156 - val sg_ref = Sign.self_ref (Theory.sign_of thy);
1.157 + val thy_ref = Theory.self_ref thy;
1.158 val ref {theorems = (space, thms), ...} = get_theorems thy;
1.159 in
1.160 fn name =>
1.161 - Option.map (map (Thm.transfer_sg (Sign.deref sg_ref))) (*semi-dynamic identity*)
1.162 - (Symtab.lookup (thms, NameSpace.intern space name)) (*static content*)
1.163 + Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*)
1.164 + (Symtab.lookup (thms, NameSpace.intern space name)) (*static content*)
1.165 end;
1.166
1.167 fun get_thms_closure thy =
1.168 - let val closures = map lookup_thms (thy :: Theory.ancestors_of thy)
1.169 - in fn namei as (name, _) => select_thm namei
1.170 - (the_thms name (get_first (fn f => f name) closures))
1.171 + let val closures = map lookup_thms (thy :: Theory.ancestors_of thy) in
1.172 + fn (name, i) => select_thm (name, i) (the_thms name (get_first (fn f => f name) closures))
1.173 end;
1.174
1.175 fun get_thm_closure thy =
1.176 let val get = get_thms_closure thy
1.177 - in fn namei as (name, _) => single_thm name (get namei) end;
1.178 + in fn (name, i) => single_thm name (get (name, i)) end;
1.179
1.180
1.181 -(* get_thm etc. *)
1.182 +(* get_thms etc. *)
1.183
1.184 -fun get_thms theory (namei as (name, _)) =
1.185 +fun get_thms theory (name, i) =
1.186 get_first (fn thy => lookup_thms thy name) (theory :: Theory.ancestors_of theory)
1.187 - |> the_thms name |> select_thm namei |> map (Thm.transfer theory);
1.188 + |> the_thms name |> select_thm (name, i) |> map (Thm.transfer theory);
1.189
1.190 fun get_thmss thy names = List.concat (map (get_thms thy) names);
1.191 -fun get_thm thy (namei as (name, _)) = single_thm name (get_thms thy namei);
1.192 +fun get_thm thy (name, i) = single_thm name (get_thms thy (name, i));
1.193
1.194
1.195 (* thms_containing etc. *)
1.196 @@ -254,7 +242,7 @@
1.197
1.198 (** store theorems **) (*DESTRUCTIVE*)
1.199
1.200 -(* hiding -- affects current theory node only! *)
1.201 +(* hiding -- affects current theory node only *)
1.202
1.203 fun hide_thms fully names thy =
1.204 let
1.205 @@ -266,20 +254,21 @@
1.206 (* naming *)
1.207
1.208 fun gen_names j len name =
1.209 - map (fn i => name ^ "_" ^ string_of_int i) (j+1 upto j+len);
1.210 + map (fn i => name ^ "_" ^ string_of_int i) (j + 1 upto j + len);
1.211
1.212 fun name_multi name xs = gen_names 0 (length xs) name ~~ xs;
1.213
1.214 -fun name_thm pre (p as (_, thm)) =
1.215 - if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm p;
1.216 +fun name_thm pre (name, thm) =
1.217 + if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm);
1.218
1.219 fun name_thms pre name [x] = [name_thm pre (name, x)]
1.220 | name_thms pre name xs = map (name_thm pre) (name_multi name xs);
1.221
1.222 -fun name_thmss name xs = (case filter_out (null o fst) xs of
1.223 +fun name_thmss name xs =
1.224 + (case filter_out (null o fst) xs of
1.225 [([x], z)] => [([name_thm true (name, x)], z)]
1.226 - | _ => snd (foldl_map (fn (i, (ys, z)) => (i + length ys,
1.227 - (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
1.228 + | _ => snd (foldl_map (fn (i, (ys, z)) =>
1.229 + (i + length ys, (map (name_thm true) (gen_names i (length ys) name ~~ ys), z))) (0, xs)));
1.230
1.231
1.232 (* enter_thms *)
1.233 @@ -287,33 +276,31 @@
1.234 fun warn_overwrite name = warning ("Replaced old copy of theorems " ^ quote name);
1.235 fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
1.236
1.237 -fun enter_thms _ _ _ app_att thy ("", thms) = app_att (thy, thms)
1.238 - | enter_thms sg pre_name post_name app_att thy (bname, thms) =
1.239 +fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms)
1.240 + | enter_thms pre_name post_name app_att (bname, thms) thy =
1.241 let
1.242 - val name = Sign.full_name sg bname;
1.243 - val (thy', thms') = app_att (thy, pre_name name thms);
1.244 - val named_thms = post_name name thms';
1.245 -
1.246 - val r as ref {theorems = (space, theorems), index} = get_theorems_sg sg;
1.247 - val space' = Sign.declare_name sg name space;
1.248 - val theorems' = Symtab.update ((name, named_thms), theorems);
1.249 - val index' = FactIndex.add (K false) (name, named_thms) index;
1.250 + val name = Sign.full_name thy bname;
1.251 + val r as ref {theorems = (space, theorems), index} = get_theorems thy;
1.252 + val space' = Sign.declare_name thy name space;
1.253 + val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
1.254 + val theorems' = Symtab.update ((name, thms'), theorems);
1.255 + val index' = FactIndex.add (K false) (name, thms') index;
1.256 in
1.257 (case Symtab.lookup (theorems, name) of
1.258 NONE => ()
1.259 - | SOME thms' =>
1.260 - if Thm.eq_thms (thms', named_thms) then warn_same name
1.261 + | SOME thms'' =>
1.262 + if Thm.eq_thms (thms', thms'') then warn_same name
1.263 else warn_overwrite name);
1.264 r := {theorems = (space', theorems'), index = index'};
1.265 - (thy', named_thms)
1.266 + (thy', thms')
1.267 end;
1.268
1.269
1.270 (* add_thms(s) *)
1.271
1.272 -fun add_thms_atts pre_name ((bname, thms), atts) thy =
1.273 - enter_thms (Theory.sign_of thy) pre_name (name_thms false)
1.274 - (Thm.applys_attributes o rpair atts) thy (bname, thms);
1.275 +fun add_thms_atts pre_name ((bname, thms), atts) =
1.276 + enter_thms pre_name (name_thms false)
1.277 + (Thm.applys_attributes o rpair atts) (bname, thms);
1.278
1.279 fun gen_add_thmss pre_name args theory =
1.280 foldl_map (fn (thy, arg) => add_thms_atts pre_name arg thy) (theory, args);
1.281 @@ -332,8 +319,8 @@
1.282 fun gen_note_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
1.283 let
1.284 fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
1.285 - val (thy', thms) = enter_thms (Theory.sign_of thy)
1.286 - name_thmss (name_thms false) (apsnd List.concat o foldl_map app) thy
1.287 + val (thy', thms) = thy |> enter_thms
1.288 + name_thmss (name_thms false) (apsnd List.concat o foldl_map app)
1.289 (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
1.290 in (thy', (bname, thms)) end;
1.291
1.292 @@ -355,42 +342,44 @@
1.293 in (thy', th') end;
1.294
1.295
1.296 -(* smart_store_thms *)
1.297 +(* smart_store_thms(_open) *)
1.298
1.299 -fun gen_smart_store_thms _ (name, []) =
1.300 +local
1.301 +
1.302 +fun smart_store _ (name, []) =
1.303 error ("Cannot store empty list of theorems: " ^ quote name)
1.304 - | gen_smart_store_thms name_thm (name, [thm]) =
1.305 - snd (enter_thms (Thm.sign_of_thm thm) (name_thm true) (name_thm false)
1.306 - I () (name, [thm]))
1.307 - | gen_smart_store_thms name_thm (name, thms) =
1.308 + | smart_store name_thm (name, [thm]) =
1.309 + #2 (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
1.310 + | smart_store name_thm (name, thms) =
1.311 let
1.312 - val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
1.313 - val sg_ref = Library.foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
1.314 - in snd (enter_thms (Sign.deref sg_ref) (name_thm true) (name_thm false)
1.315 - I () (name, thms))
1.316 - end;
1.317 + fun merge (thy, th) = Theory.merge (thy, Thm.theory_of_thm th);
1.318 + val thy = Library.foldl merge (Thm.theory_of_thm (hd thms), tl thms);
1.319 + in #2 (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
1.320
1.321 -val smart_store_thms = gen_smart_store_thms name_thms;
1.322 -val smart_store_thms_open = gen_smart_store_thms (K (K I));
1.323 +in
1.324 +
1.325 +val smart_store_thms = smart_store name_thms;
1.326 +val smart_store_thms_open = smart_store (K (K I));
1.327 +
1.328 +end;
1.329
1.330
1.331 (* forall_elim_vars (belongs to drule.ML) *)
1.332
1.333 (*Replace outermost quantified variable by Var of given index.*)
1.334 fun forall_elim_var i th =
1.335 - let val {prop,sign,...} = rep_thm th
1.336 - in case prop of
1.337 + let val {prop, thy, ...} = Thm.rep_thm th
1.338 + in case prop of
1.339 Const ("all", _) $ Abs (a, T, _) =>
1.340 let val used = map (fst o fst)
1.341 (List.filter (equal i o snd o fst) (Term.add_vars ([], prop)))
1.342 - in forall_elim (cterm_of sign (Var ((variant used a, i), T))) th end
1.343 - | _ => raise THM ("forall_elim_var", i, [th])
1.344 - end;
1.345 + in Thm.forall_elim (Thm.cterm_of thy (Var ((variant used a, i), T))) th end
1.346 + | _ => raise THM ("forall_elim_var", i, [th])
1.347 + end;
1.348
1.349 (*Repeat forall_elim_var until all outer quantifiers are removed*)
1.350 fun forall_elim_vars i th =
1.351 - forall_elim_vars i (forall_elim_var i th)
1.352 - handle THM _ => th;
1.353 + forall_elim_vars i (forall_elim_var i th) handle THM _ => th;
1.354
1.355
1.356 (* store axioms as theorems *)
1.357 @@ -428,86 +417,17 @@
1.358
1.359
1.360
1.361 -(*** derived theory operations ***)
1.362 -
1.363 -(** theory management **)
1.364 -
1.365 -(* data kind 'Pure/theory_management' *)
1.366 -
1.367 -structure TheoryManagementDataArgs =
1.368 -struct
1.369 - val name = "Pure/theory_management";
1.370 - type T = {name: string, version: int};
1.371 -
1.372 - val empty = {name = "", version = 0};
1.373 - val copy = I;
1.374 - val prep_ext = I;
1.375 - fun merge _ = empty;
1.376 - fun print _ _ = ();
1.377 -end;
1.378 -
1.379 -structure TheoryManagementData = TheoryDataFun(TheoryManagementDataArgs);
1.380 -val get_info = TheoryManagementData.get;
1.381 -val put_info = TheoryManagementData.put;
1.382 -
1.383 -
1.384 -(* get / put name *)
1.385 -
1.386 -val get_name = #name o get_info;
1.387 -fun put_name name = put_info {name = name, version = 0};
1.388 -
1.389 -
1.390 -(* control prefixing of theory name *)
1.391 -
1.392 -val global_path = Theory.root_path;
1.393 -
1.394 -fun local_path thy =
1.395 - thy |> Theory.root_path |> Theory.add_path (get_name thy);
1.396 -
1.397 -
1.398 -(* begin / end theory *)
1.399 -
1.400 -fun begin_theory name thys =
1.401 - Theory.prep_ext_merge thys
1.402 - |> put_name name
1.403 - |> local_path;
1.404 -
1.405 -fun end_theory thy =
1.406 - thy
1.407 - |> Theory.add_name (get_name thy);
1.408 -
1.409 -fun checkpoint thy =
1.410 - if is_draft thy then
1.411 - let val {name, version} = get_info thy in
1.412 - thy
1.413 - |> Theory.add_name (name ^ ":" ^ string_of_int version)
1.414 - |> put_info {name = name, version = version + 1}
1.415 - end
1.416 - else thy;
1.417 -
1.418 -
1.419 -
1.420 -(** add logical types **)
1.421 -
1.422 -fun add_typedecls decls thy =
1.423 - let
1.424 - val full = Sign.full_name (Theory.sign_of thy);
1.425 -
1.426 - fun type_of (raw_name, vs, mx) =
1.427 - if null (duplicates vs) then (raw_name, length vs, mx)
1.428 - else error ("Duplicate parameters in type declaration: " ^ quote raw_name);
1.429 - in thy |> Theory.add_types (map type_of decls) end;
1.430 -
1.431 -
1.432 -
1.433 (*** the ProtoPure theory ***)
1.434
1.435 +val aT = TFree ("'a", []);
1.436 +val A = Free ("A", propT);
1.437 +
1.438 val proto_pure =
1.439 - Theory.pre_pure
1.440 - |> TheoryManagementData.init |> put_name "ProtoPure"
1.441 + Context.pre_pure
1.442 + |> Sign.init
1.443 + |> Theory.init
1.444 + |> Proofterm.init
1.445 |> TheoremsData.init
1.446 - |> Proofterm.init
1.447 - |> global_path
1.448 |> Theory.add_types
1.449 [("fun", 2, NoSyn),
1.450 ("prop", 0, NoSyn),
1.451 @@ -518,30 +438,30 @@
1.452 |> Theory.add_syntax Syntax.pure_appl_syntax
1.453 |> Theory.add_modesyntax (Symbol.xsymbolsN, true) Syntax.pure_xsym_syntax
1.454 |> Theory.add_syntax
1.455 - [("==>", "[prop, prop] => prop", Delimfix "op ==>"),
1.456 + [("==>", "prop => prop => prop", Delimfix "op ==>"),
1.457 (Term.dummy_patternN, "aprop", Delimfix "'_")]
1.458 |> Theory.add_consts
1.459 - [("==", "['a, 'a] => prop", InfixrName ("==", 2)),
1.460 - ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
1.461 + [("==", "'a => 'a => prop", InfixrName ("==", 2)),
1.462 + ("==>", "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
1.463 ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
1.464 ("Goal", "prop => prop", NoSyn),
1.465 ("TYPE", "'a itself", NoSyn),
1.466 (Term.dummy_patternN, "'a", Delimfix "'_")]
1.467 |> Theory.add_finals_i false
1.468 - [Const("==", [TFree ("'a", []), TFree ("'a", [])] ---> propT),
1.469 - Const("==>", [propT, propT] ---> propT),
1.470 - Const("all", (TFree("'a", []) --> propT) --> propT),
1.471 - Const("TYPE", a_itselfT)]
1.472 + [Const ("==", [aT, aT] ---> propT),
1.473 + Const ("==>", [propT, propT] ---> propT),
1.474 + Const ("all", (aT --> propT) --> propT),
1.475 + Const ("TYPE", a_itselfT)]
1.476 |> Theory.add_modesyntax ("", false)
1.477 (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
1.478 |> Theory.add_trfuns Syntax.pure_trfuns
1.479 |> Theory.add_trfunsT Syntax.pure_trfunsT
1.480 - |> local_path
1.481 + |> Sign.local_path
1.482 |> (#1 oo (add_defs_i false o map Thm.no_attributes))
1.483 - [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
1.484 + [("Goal_def", Logic.mk_equals (Logic.mk_goal A, A))]
1.485 |> (#1 o add_thmss [(("nothing", []), [])])
1.486 |> Theory.add_axioms_i Proofterm.equality_axms
1.487 - |> end_theory;
1.488 + |> Context.end_theory;
1.489
1.490 structure ProtoPure =
1.491 struct