tuned for uniformity

--- a/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 21 10:41:18 2013 +0200
@@ -819,22 +819,28 @@
 
 local
 
-fun note_eqns_register deps witss attrss eqns export export' =
-  Attrib.generic_notes Thm.lemmaK
-    (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns)
-  #-> (fn facts => `(fn context => meta_rewrite (Context.proof_of context) (maps snd facts)))
-  #-> (fn eqns => fold (fn ((dep, morph), wits) =>
-    fn context =>
+fun note_eqns_register deps witss attrss eqns export export' context =
+  let
+    val facts = 
+      (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
+    val (eqns', context') = context 
+      |> Attrib.generic_notes Thm.lemmaK facts
+      |-> (fn facts' => `(fn context'' => meta_rewrite (Context.proof_of context'') (maps snd facts')));
+  in
+    context'
+    |> fold2 (fn (dep, morph) => fn wits => fn context'' =>
       Locale.add_registration
         (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
-        (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true))
-        export context) (deps ~~ witss));
+        (Element.eq_morphism (Context.theory_of context'') eqns' |> Option.map (rpair true))
+        export context'') deps witss
+  end;
 
 fun gen_interpretation prep_expr parse_prop prep_attr
     expression equations thy =
   let
-    val ((propss, deps, export), expr_ctxt) = Proof_Context.init_global thy
-      |> prep_expr expression;
+    val initial_ctxt = Proof_Context.init_global thy;
+
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
     val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;
@@ -891,27 +897,27 @@
   let
     val facts =
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
-    val eqns' = ctxt
+    val (eqns', _) = ctxt (* FIXME duplication to add_thmss *)
       |> Attrib.local_notes Thm.lemmaK facts
-      |-> (fn facts => `(fn ctxt => meta_rewrite ctxt (maps snd facts)))
-      |> fst;  (* FIXME duplication to add_thmss *)
+      |-> (fn facts' => `(fn ctxt'' => meta_rewrite ctxt'' (maps snd facts')));
   in
     ctxt
     |> Locale.add_thmss target Thm.lemmaK (Attrib.partial_evaluation ctxt facts)
-    |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) =>
+    |> Proof_Context.background_theory (fold2 (fn (dep, morph) => fn wits =>
       fn thy =>
         Locale.add_dependency target
           (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))
           (Element.eq_morphism thy eqns' |> Option.map (rpair true))
-          export thy) (deps ~~ witss))
+          export thy) deps witss)
   end;
 
 fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
     before_exit raw_target expression equations thy =
   let
     val target = prep_loc thy raw_target;
-    val target_ctxt = Named_Target.init before_exit target thy;
-    val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
+    val initial_ctxt = Named_Target.init before_exit target thy;
+
+    val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
 
     val attrss = map (apsnd (map (prep_attr thy)) o fst) equations;

--- a/src/Pure/Isar/locale.ML	Sun Apr 21 10:41:18 2013 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Apr 21 10:41:18 2013 +0200
@@ -458,14 +458,15 @@
     val thy = Context.theory_of context;
     val regs = Registrations.get context |> fst;
     val base = instance_of thy name (morph $> export);
+    val serial' = case Idtab.lookup regs (name, base) of
+        NONE =>
+          error ("No interpretation of locale " ^
+            quote (extern thy name) ^ " with\nparameter instantiation " ^
+            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
+            " available")
+      | SOME (_, serial') => serial';
   in
-    (case Idtab.lookup regs (name, base) of
-      NONE =>
-        error ("No interpretation of locale " ^
-          quote (extern thy name) ^ " with\nparameter instantiation " ^
-          space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
-          " available")
-    | SOME (_, serial') => add_mixin serial' mixin context)
+    add_mixin serial' mixin context
   end;
 
 (* Note that a registration that would be subsumed by an existing one will not be
@@ -477,13 +478,15 @@
     val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     val morph = base_morph $> mix;
     val inst = instance_of thy name morph;
+    val idents = Idents.get context;
   in
-    if redundant_ident thy (Idents.get context) (name, inst)
+    if redundant_ident thy idents (name, inst)
     then context  (* FIXME amend mixins? *)
     else
-      (Idents.get context, context)
+      (idents, context)
       (* add new registrations with inherited mixins *)
-      |> (snd o roundup thy (add_reg thy export) export (name, morph))
+      |> roundup thy (add_reg thy export) export (name, morph)
+      |> snd
       (* add mixin *)
       |> (case mixin of NONE => I | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)