# HG changeset patch
# User ballarin
# Date 1519997319 -3600
# Node ID d5a7f2c5465552d67c7ba51c021f21235aaa0a2a
# Parent  b6ce18784872e0810fbfba8b5b892c22c2df7e67
Fall back to reading rewrite morphism first if activation fails without it.

diff -r b6ce18784872 -r d5a7f2c54655 NEWS
--- a/NEWS	Fri Mar 02 14:19:25 2018 +0100
+++ b/NEWS	Fri Mar 02 14:28:39 2018 +0100
@@ -180,6 +180,11 @@
 'for' now needs to occur after, not before 'rewrites'.
 Minor INCOMPATIBILITY.
 
+* For rewrites clauses in locale expressions, if activating a locale
+instance fails, fall back to reading the clause first.  This helps
+avoiding qualified locale instances where the qualifier's sole purpose
+is avoiding duplicate constant declarations.
+
 
 *** Pure ***
 
diff -r b6ce18784872 -r d5a7f2c54655 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Mar 02 14:19:25 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Mar 02 14:28:39 2018 +0100
@@ -394,7 +394,9 @@
         val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
-        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2; (* may fail *)
+        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
+          handle ERROR msg => if null eqns then error msg else
+            (writeln (msg ^ "\nFalling back to reading rewrites clause first."); ctxt2);
 
         val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
         val eqns' = (prep_eqns ctxt' o map snd) eqns;
@@ -405,7 +407,8 @@
           |> Variable.export_terms ctxt' ctxt
           |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
           |> the_default Morphism.identity;
-       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
+       val ctxt'' = if null eqns then ctxt' else 
+         Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
        val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
       in (i + 1, insts', eqnss', ctxt'') end;