Fall back to reading rewrite morphism first if activation fails without it.
authorballarin
Fri Mar 02 14:28:39 2018 +0100 (16 months ago)
changeset 67741d5a7f2c54655
parent 67740 b6ce18784872
child 67742 6306bd582957
Fall back to reading rewrite morphism first if activation fails without it.
NEWS
src/Pure/Isar/expression.ML
     1.1 --- a/NEWS	Fri Mar 02 14:19:25 2018 +0100
     1.2 +++ b/NEWS	Fri Mar 02 14:28:39 2018 +0100
     1.3 @@ -180,6 +180,11 @@
     1.4  'for' now needs to occur after, not before 'rewrites'.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* For rewrites clauses in locale expressions, if activating a locale
     1.8 +instance fails, fall back to reading the clause first.  This helps
     1.9 +avoiding qualified locale instances where the qualifier's sole purpose
    1.10 +is avoiding duplicate constant declarations.
    1.11 +
    1.12  
    1.13  *** Pure ***
    1.14  
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Mar 02 14:19:25 2018 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Fri Mar 02 14:28:39 2018 +0100
     2.3 @@ -394,7 +394,9 @@
     2.4          val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
     2.5          val inst''' = insts'' |> List.last |> snd |> snd;
     2.6          val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
     2.7 -        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2; (* may fail *)
     2.8 +        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2
     2.9 +          handle ERROR msg => if null eqns then error msg else
    2.10 +            (writeln (msg ^ "\nFalling back to reading rewrites clause first."); ctxt2);
    2.11  
    2.12          val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
    2.13          val eqns' = (prep_eqns ctxt' o map snd) eqns;
    2.14 @@ -405,7 +407,8 @@
    2.15            |> Variable.export_terms ctxt' ctxt
    2.16            |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
    2.17            |> the_default Morphism.identity;
    2.18 -       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
    2.19 +       val ctxt'' = if null eqns then ctxt' else 
    2.20 +         Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
    2.21         val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
    2.22        in (i + 1, insts', eqnss', ctxt'') end;
    2.23