# HG changeset patch # User wenzelm # Date 1331416832 -3600 # Node ID 6eb62a79d02acc67b3746282ff71cf33797502d9 # Parent 56376f6be74f7941c79a316c2b1070e9927d311b# Parent ef45df55127dbaf7ab85a80b2c987c769906008e merged diff -r 56376f6be74f -r 6eb62a79d02a doc-src/Locales/Locales/Examples.thy --- 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 = diff -r 56376f6be74f -r 6eb62a79d02a doc-src/Locales/Locales/Examples3.thy --- 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 \"}. 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 "\''" 50) where "meet' \ le'.meet" abbreviation join' (infixl "\''" 50) where "join' \ 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 \ order_preserving proof unfold_locales + sublocale lattice_hom \ order_preserving + proof unfold_locales fix x y assume "x \ y" then have "y = (x \ y)" by (simp add: le.join_connection) @@ -481,7 +483,7 @@ locale fun_lattice = fun_partial_order + lattice sublocale fun_lattice \ f: lattice "\f g. \x. f x \ g x" - proof unfold_locales + proof unfold_locales fix f g have "partial_order.is_inf (\f g. \x. f x \ g x) f g (\x. f x \ g x)" apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done diff -r 56376f6be74f -r 6eb62a79d02a doc-src/Locales/Locales/document/Examples.tex --- 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 diff -r 56376f6be74f -r 6eb62a79d02a doc-src/Locales/Locales/document/Examples3.tex --- 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 diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/Isar/class_declaration.ML --- 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); diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/Isar/element.ML --- 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 *) diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/Isar/expression.ML --- 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; diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/Isar/locale.ML --- 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; diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/more_thm.ML --- 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; diff -r 56376f6be74f -r 6eb62a79d02a src/Pure/pattern.ML --- 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); diff -r 56376f6be74f -r 6eb62a79d02a src/Tools/interpretation_with_defs.ML --- 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))