--- a/src/Pure/Isar/locale.ML Sat Jun 24 17:42:50 2017 +0200
+++ b/src/Pure/Isar/locale.ML Sat Jun 24 17:44:26 2017 +0200
@@ -432,8 +432,10 @@
grouped 100 Par_List.map
(Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
in
- fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
- notes' input
+ input
+ |> fold_rev
+ (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes'
+ handle ERROR msg => activate_err msg (name, morph) context
end;
fun activate_all name thy activ_elem transfer (marked, input) =