Fall back to reading rewrite morphism first if activation fails without it.

--- 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 ***
 

--- 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;