--- a/doc-src/Locales/Locales/Examples.thy Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/Examples.thy Sat Mar 10 23:00:32 2012 +0100
@@ -193,7 +193,8 @@
notions of infimum and supremum for partial orders are introduced,
together with theorems about their uniqueness. *}
- context partial_order begin
+ context partial_order
+ begin
definition
is_inf where "is_inf x y i =
--- a/doc-src/Locales/Locales/Examples3.thy Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Sat Mar 10 23:00:32 2012 +0100
@@ -10,8 +10,8 @@
discharge the premise in the definition of @{text "op \<sqsubset>"}. In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
- context of the locale. Therefore is would be convenient to have the
- interpreted locale conclusions temporary available in the proof.
+ context of the locale. Therefore it would be convenient to have the
+ interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}. We
repeat the example from the previous section to illustrate this. *}
@@ -304,7 +304,8 @@
second lattice.
*}
- context lattice_hom begin
+ context lattice_hom
+ begin
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
end
@@ -369,7 +370,8 @@
preserving. As the final example of this section, a locale
interpretation is used to assert this: *}
- sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
+ sublocale lattice_hom \<subseteq> order_preserving
+ proof unfold_locales
fix x y
assume "x \<sqsubseteq> y"
then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
@@ -481,7 +483,7 @@
locale fun_lattice = fun_partial_order + lattice
sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
- proof unfold_locales
+ proof unfold_locales
fix f g
have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
--- a/doc-src/Locales/Locales/document/Examples.tex Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex Sat Mar 10 23:00:32 2012 +0100
@@ -253,7 +253,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ partial{\isaliteral{5F}{\isacharunderscore}}order\ \isakeyword{begin}\isanewline
+\ partial{\isaliteral{5F}{\isacharunderscore}}order\isanewline
+\ \ \isakeyword{begin}\isanewline
\isanewline
\ \ \isacommand{definition}\isamarkupfalse%
\isanewline
--- a/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Sat Mar 10 23:00:32 2012 +0100
@@ -34,8 +34,8 @@
discharge the premise in the definition of \isa{op\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}}. In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
- context of the locale. Therefore is would be convenient to have the
- interpreted locale conclusions temporary available in the proof.
+ context of the locale. Therefore it would be convenient to have the
+ interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}. We
repeat the example from the previous section to illustrate this.%
@@ -439,7 +439,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ \isakeyword{begin}\isanewline
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\isanewline
+\ \ \isakeyword{begin}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C7371696E7465723E}{\isasymsqinter}}{\isaliteral{27}{\isacharprime}}{\isaliteral{27}{\isacharprime}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{5}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}meet{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ le{\isaliteral{27}{\isacharprime}}{\isaliteral{2E}{\isachardot}}meet{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -513,9 +514,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving%
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving\isanewline
+%
\isadelimproof
-\ %
+\ \ %
\endisadelimproof
%
\isatagproof
@@ -738,7 +740,7 @@
\ fun{\isaliteral{5F}{\isacharunderscore}}lattice\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
-\ \ \ \ %
+\ \ %
\endisadelimproof
%
\isatagproof
--- a/src/Pure/Isar/class_declaration.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sat Mar 10 23:00:32 2012 +0100
@@ -74,13 +74,12 @@
val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
val const_eq_morph =
(case eq_morph of
- SOME eq_morph => const_morph $> eq_morph
+ SOME eq_morph => const_morph $> eq_morph
| NONE => const_morph);
val thm'' = Morphism.thm const_eq_morph thm';
val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
- val assm_intro = Option.map prove_assm_intro
- (fst (Locale.intros_of thy class));
+ val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
(* of_class *)
val of_class_prop_concl = Logic.mk_of_class (aT, class);
--- a/src/Pure/Isar/element.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/element.ML Sat Mar 10 23:00:32 2012 +0100
@@ -461,11 +461,13 @@
(* rewriting with equalities *)
-fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
- {binding = [],
- typ = [],
- term = [Raw_Simplifier.rewrite_term thy thms []],
- fact = [map (Raw_Simplifier.rewrite_rule thms)]});
+fun eq_morphism _ [] = NONE
+ | eq_morphism thy thms =
+ SOME (Morphism.morphism
+ {binding = [],
+ typ = [],
+ term = [Raw_Simplifier.rewrite_term thy thms []],
+ fact = [map (Raw_Simplifier.rewrite_rule thms)]});
(* transfer to theory using closure *)
--- a/src/Pure/Isar/expression.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/expression.ML Sat Mar 10 23:00:32 2012 +0100
@@ -814,17 +814,15 @@
local
-fun note_eqns_register deps witss attrss eqns export export' context =
- context
- |> Element.generic_note_thmss Thm.lemmaK
+fun note_eqns_register deps witss attrss eqns export export' =
+ Element.generic_note_thmss Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
- |-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
- |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+ #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
+ #-> (fn eqns => fold (fn ((dep, morph), wits) =>
fn context =>
- Locale.add_registration (dep, morph $> Element.satisfy_morphism
- (map (Element.transform_witness export') wits))
- (Element.eq_morphism (Context.theory_of context) eqns |>
- Option.map (rpair true))
+ Locale.add_registration
+ (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
+ (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
export context) (deps ~~ witss));
fun gen_interpretation prep_expr parse_prop prep_attr
@@ -899,8 +897,7 @@
|> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
fn thy =>
Locale.add_dependency target
- (dep, morph $> Element.satisfy_morphism
- (map (Element.transform_witness export') wits))
+ (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
(Element.eq_morphism thy eqns' |> Option.map (rpair true))
export thy) (deps ~~ witss))
end;
--- a/src/Pure/Isar/locale.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/locale.ML Sat Mar 10 23:00:32 2012 +0100
@@ -99,17 +99,16 @@
lists indexed by registration/dependency serial,
entries for empty lists may be omitted *)
-fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial');
+fun lookup_mixins serial' mixins = Inttab.lookup_list mixins serial';
-fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2);
+fun merge_mixins mixs : mixins = Inttab.merge_list (eq_snd op =) mixs;
-fun insert_mixin serial' mixin =
- Inttab.map_default (serial', []) (cons (mixin, serial ()));
+fun insert_mixin serial' mixin = Inttab.cons_list (serial', (mixin, serial ()));
fun rename_mixin (old, new) mix =
- case Inttab.lookup mix old of
- NONE => mix |
- SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
+ (case Inttab.lookup mix old of
+ NONE => mix
+ | SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs));
fun compose_mixins mixins =
fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
@@ -241,43 +240,23 @@
(*** Identifiers: activated locales in theory or proof context ***)
-(* subsumption *)
-fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
- (* smaller term is more general *)
+type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *)
-(* total order *)
-fun ident_ord ((n: string, ts), (m, ss)) =
- (case fast_string_ord (m, n) of
- EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
- | ord => ord);
+val empty_idents : idents = Symtab.empty;
+val insert_idents = Symtab.insert_list (eq_list (op aconv));
+val merge_idents = Symtab.merge_list (eq_list (op aconv));
-local
+fun redundant_ident thy idents (name, instance) =
+ exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name);
-datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
-
-structure Identifiers = Generic_Data
+structure Idents = Generic_Data
(
- type T = (string * term list) list delayed;
- val empty = Ready [];
+ type T = idents;
+ val empty = empty_idents;
val extend = I;
- val merge = ToDo;
+ val merge = merge_idents;
);
-fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
- | finish _ (Ready ids) = ids;
-
-val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
- (case Identifiers.get (Context.Theory thy) of
- Ready _ => NONE
- | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
-
-in
-
-val get_idents = (fn Ready ids => ids) o Identifiers.get;
-val put_idents = Identifiers.put o Ready;
-
-end;
-
(** Resolve locale dependencies in a depth-first fashion **)
@@ -292,8 +271,7 @@
let
val instance = instance_of thy name (morph $> stem $> export);
in
- if member (ident_le thy) marked (name, instance)
- then (deps, marked)
+ if redundant_ident thy marked (name, instance) then (deps, marked)
else
let
val full_morph = morph $> compose_mixins mixins $> stem;
@@ -301,7 +279,7 @@
val dependencies = dependencies_of thy name |>
map (fn ((name', (morph', export')), serial') =>
(name', morph' $> export', mixins_of thy name serial'));
- val marked' = (name, instance) :: marked;
+ val marked' = insert_idents (name, instance) marked;
val (deps', marked'') =
fold_rev (add thy (depth + 1) full_morph export) dependencies
([], marked');
@@ -320,12 +298,12 @@
(* Find all dependencies including new ones (which are dependencies enriching
existing registrations). *)
val (dependencies, marked') =
- add thy 0 Morphism.identity export (name, morph, []) ([], []);
+ add thy 0 Morphism.identity export (name, morph, []) ([], empty_idents);
(* Filter out fragments from marked; these won't be activated. *)
val dependencies' = filter_out (fn (name, morph) =>
- member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
+ redundant_ident thy marked (name, instance_of thy name (morph $> export))) dependencies;
in
- (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
+ (merge_idents (marked, marked'), input |> fold_rev activate_dep dependencies')
end;
end;
@@ -333,7 +311,9 @@
(*** Registrations: interpretations in theories or proof contexts ***)
-structure Idtab = Table(type key = string * term list val ord = ident_ord);
+val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord);
+
+structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
structure Registrations = Generic_Data
(
@@ -385,13 +365,15 @@
val thy = Context.theory_of context;
in
roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
- Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
+ Morphism.identity (name, morph)
+ (insert_idents (name, instance_of thy name morph) empty_idents, [])
|> snd |> filter (snd o fst) (* only inheritable mixins *)
|> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
|> compose_mixins
end;
-fun get_registrations context select = Registrations.get context
+fun get_registrations context select =
+ Registrations.get context
|>> Idtab.dest |>> select
(* with inherited mixins *)
|-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
@@ -454,8 +436,8 @@
let
val thy = Context.theory_of context;
in
- roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
- |-> put_idents
+ roundup thy activate_syntax_decls Morphism.identity dep (Idents.get context, context)
+ |-> Idents.put
end);
fun activate_facts export dep context =
@@ -464,14 +446,14 @@
val activate =
activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
in
- roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
- dep (get_idents context, context)
- |-> put_idents
+ roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
+ |-> Idents.put
end;
fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
- ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of;
+ (empty_idents, Context.Proof (Proof_Context.init_global thy))
+ |-> Idents.put |> Context.proof_of;
(*** Add and extend registrations ***)
@@ -501,10 +483,10 @@
val morph = base_morph $> mix;
val inst = instance_of thy name morph;
in
- if member (ident_le thy) (get_idents context) (name, inst)
+ if redundant_ident thy (Idents.get context) (name, inst)
then context (* FIXME amend mixins? *)
else
- (get_idents context, context)
+ (Idents.get context, context)
(* add new registrations with inherited mixins *)
|> roundup thy (add_reg thy export) export (name, morph)
|> snd
@@ -526,7 +508,7 @@
val deps = dependencies_of thy loc;
in
case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
- ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
+ total_ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
NONE => error ("Locale " ^
quote (extern thy name) ^ " with\parameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
@@ -543,8 +525,9 @@
(apfst (cons ((name, (morph, export)), serial')) #>
apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
val context' = Context.Theory thy';
- val (_, regs) = fold_rev (roundup thy' cons export)
- (registrations_of context' loc) (get_idents (context'), []);
+ val (_, regs) =
+ fold_rev (roundup thy' cons export)
+ (registrations_of context' loc) (Idents.get context', []);
in
thy'
|> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
@@ -644,7 +627,7 @@
fun cons_elem (elem as Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
val elems =
- activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
+ activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, [])
|> snd |> rev;
in
Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
@@ -658,23 +641,23 @@
val _ = the_locale thy name; (* error if locale unknown *)
in
(case registrations_of (Context.Proof ctxt) (* FIXME *) name of
- [] => Pretty.str ("no interpretations")
+ [] => Pretty.str "no interpretations"
| regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
end |> Pretty.writeln;
fun print_dependencies ctxt clean export insts =
let
val thy = Proof_Context.theory_of ctxt;
- val idents = if clean then [] else get_idents (Context.Proof ctxt);
+ val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt);
in
(case fold (roundup thy cons export) insts (idents, []) |> snd of
- [] => Pretty.str ("no dependencies")
+ [] => Pretty.str "no dependencies"
| deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
end |> Pretty.writeln;
fun locale_deps thy =
let
- val names = all_locales thy
+ val names = all_locales thy;
fun add_locale_node name =
let
val params = params_of thy name;
@@ -690,7 +673,8 @@
val dependencies =
map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
in
- fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+ fold (fn (super, ts) => fn (gr, deps) =>
+ (gr |> Graph.add_edge (super, name),
deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
dependencies
end;
--- a/src/Pure/more_thm.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/more_thm.ML Sat Mar 10 23:00:32 2012 +0100
@@ -37,7 +37,6 @@
val thm_cache: (thm -> 'a) -> thm -> 'a
val is_reflexive: thm -> bool
val eq_thm: thm * thm -> bool
- val eq_thms: thm list * thm list -> bool
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val equiv_thm: thm * thm -> bool
@@ -188,8 +187,6 @@
Context.joinable (pairself Thm.theory_of_thm ths) andalso
is_equal (thm_ord ths);
-val eq_thms = eq_list eq_thm;
-
val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;
--- a/src/Pure/pattern.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/pattern.ML Sat Mar 10 23:00:32 2012 +0100
@@ -399,7 +399,9 @@
fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
-fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+fun matchess thy (ps, os) =
+ length ps = length os andalso
+ ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
--- a/src/Tools/interpretation_with_defs.ML Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML Sat Mar 10 23:00:32 2012 +0100
@@ -17,20 +17,19 @@
structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
struct
-fun note_eqns_register deps witss def_eqns attrss eqns export export' context =
+fun note_eqns_register deps witss def_eqns attrss eqns export export' =
let
fun meta_rewrite context =
map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
maps snd;
in
- context
- |> Element.generic_note_thmss Thm.lemmaK
+ Element.generic_note_thmss Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
- |-> (fn facts => `(fn context => meta_rewrite context facts))
- |-> (fn eqns => fold (fn ((dep, morph), wits) =>
+ #-> (fn facts => `(fn context => meta_rewrite context facts))
+ #-> (fn eqns => fold (fn ((dep, morph), wits) =>
fn context =>
- Locale.add_registration (dep, morph $> Element.satisfy_morphism
- (map (Element.transform_witness export') wits))
+ Locale.add_registration
+ (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
(Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
Option.map (rpair true))
export context) (deps ~~ witss))