1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 10:12:44 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 14:21:42 2008 +0100
     1.3 @@ -148,6 +148,27 @@
     1.4  
     1.5  end
     1.6  
     1.7 +
     1.8 +text {* Notes *}
     1.9 +
    1.10 +(* A somewhat arcane homomorphism example *)
    1.11 +
    1.12 +definition semi_hom where
    1.13 +  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
    1.14 +
    1.15 +lemma semi_hom_mult:
    1.16 +  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
    1.17 +  by (simp add: semi_hom_def)
    1.18 +
    1.19 +locale semi_hom_loc = prod: semi prod + sum: semi sum
    1.20 +  for prod and sum and h +
    1.21 +  assumes semi_homh: "semi_hom(prod, sum, h)"
    1.22 +  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
    1.23 +
    1.24 +lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
    1.25 +  by (rule semi_hom_mult)
    1.26 +
    1.27 +
    1.28  text {* Theorem statements *}
    1.29  
    1.30  lemma (in lgrp) lcancel:

     2.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 10 10:12:44 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 14:21:42 2008 +0100
     2.3 @@ -487,7 +487,6 @@
     2.4        NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
     2.5      val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
     2.6    in ((fixed, deps, elems'), (parms, spec, defs)) end;
     2.7 -  (* FIXME check if defs used somewhere *)
     2.8  
     2.9  in
    2.10  
    2.11 @@ -695,13 +694,14 @@
    2.12      val _ = if null extraTs then ()
    2.13        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    2.14  
    2.15 -    val satisfy = Element.satisfy_morphism b_axioms;
    2.16 +    val a_satisfy = Element.satisfy_morphism a_axioms;
    2.17 +    val b_satisfy = Element.satisfy_morphism b_axioms;
    2.18  
    2.19      val params = fixed @
    2.20        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
    2.21      val asm = if is_some b_statement then b_statement else a_statement;
    2.22 -    val body_elems' = map (defines_to_notes thy') body_elems;
    2.23  
    2.24 +    (* These are added immediately. *)
    2.25      val notes =
    2.26          if is_some asm
    2.27          then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
    2.28 @@ -709,7 +709,16 @@
    2.29              [(Attrib.internal o K) NewLocale.witness_attrib])])])]
    2.30          else [];
    2.31  
    2.32 -    val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
    2.33 +    (* These will be added in the local theory. *)
    2.34 +    val notes' = body_elems |>
    2.35 +      map (defines_to_notes thy') |>
    2.36 +      map (Element.morph_ctxt a_satisfy) |>
    2.37 +      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    2.38 +      fst |>
    2.39 +      map (Element.morph_ctxt b_satisfy) |>
    2.40 +      map_filter (fn Notes notes => SOME notes | _ => NONE);
    2.41 +
    2.42 +    val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
    2.43  
    2.44      val loc_ctxt = thy' |>
    2.45        NewLocale.register_locale bname (extraTs, params)
    2.46 @@ -717,12 +726,6 @@
    2.47          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
    2.48        NewLocale.init name;
    2.49  
    2.50 -    (* These will be added in the local theory. *)
    2.51 -    val notes' = body_elems' |>
    2.52 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    2.53 -      fst |> map (Element.morph_ctxt satisfy) |>
    2.54 -      map_filter (fn Notes notes => SOME notes | _ => NONE);
    2.55 -
    2.56    in ((name, notes'), loc_ctxt) end;
    2.57  
    2.58  in