# HG changeset patch
# User ballarin
# Date 1228915302 -3600
# Node ID b0a0843dfd9905648a7823e1a5eadf7d8c55ae92
# Parent  3dc51c01f9f31ed50884335beb47e1de4d451cd8
Satisfy a_axioms.

diff -r 3dc51c01f9f3 -r b0a0843dfd99 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 10:12:44 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Wed Dec 10 14:21:42 2008 +0100
@@ -148,6 +148,27 @@
 
 end
 
+
+text {* Notes *}
+
+(* A somewhat arcane homomorphism example *)
+
+definition semi_hom where
+  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
+
+lemma semi_hom_mult:
+  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
+  by (simp add: semi_hom_def)
+
+locale semi_hom_loc = prod: semi prod + sum: semi sum
+  for prod and sum and h +
+  assumes semi_homh: "semi_hom(prod, sum, h)"
+  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
+
+lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
+  by (rule semi_hom_mult)
+
+
 text {* Theorem statements *}
 
 lemma (in lgrp) lcancel:
diff -r 3dc51c01f9f3 -r b0a0843dfd99 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Dec 10 10:12:44 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 10 14:21:42 2008 +0100
@@ -487,7 +487,6 @@
       NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
     val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
   in ((fixed, deps, elems'), (parms, spec, defs)) end;
-  (* FIXME check if defs used somewhere *)
 
 in
 
@@ -695,13 +694,14 @@
     val _ = if null extraTs then ()
       else warning ("Additional type variable(s) in locale specification " ^ quote bname);
 
-    val satisfy = Element.satisfy_morphism b_axioms;
+    val a_satisfy = Element.satisfy_morphism a_axioms;
+    val b_satisfy = Element.satisfy_morphism b_axioms;
 
     val params = fixed @
       (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
     val asm = if is_some b_statement then b_statement else a_statement;
-    val body_elems' = map (defines_to_notes thy') body_elems;
 
+    (* These are added immediately. *)
     val notes =
         if is_some asm
         then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
@@ -709,7 +709,16 @@
             [(Attrib.internal o K) NewLocale.witness_attrib])])])]
         else [];
 
-    val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
+    (* These will be added in the local theory. *)
+    val notes' = body_elems |>
+      map (defines_to_notes thy') |>
+      map (Element.morph_ctxt a_satisfy) |>
+      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
+      fst |>
+      map (Element.morph_ctxt b_satisfy) |>
+      map_filter (fn Notes notes => SOME notes | _ => NONE);
+
+    val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
 
     val loc_ctxt = thy' |>
       NewLocale.register_locale bname (extraTs, params)
@@ -717,12 +726,6 @@
         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
       NewLocale.init name;
 
-    (* These will be added in the local theory. *)
-    val notes' = body_elems' |>
-      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
-      fst |> map (Element.morph_ctxt satisfy) |>
-      map_filter (fn Notes notes => SOME notes | _ => NONE);
-
   in ((name, notes'), loc_ctxt) end;
 
 in