diff -r 9b535493ac8d -r d2d0b9b1a69d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Oct 01 07:40:25 2009 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Oct 01 20:37:33 2009 +0200
@@ -68,8 +68,10 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
-  val add_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
-  val amend_registration: string * morphism -> morphism * bool -> morphism -> theory -> theory
+  val add_registration: string * morphism -> (morphism * bool) option ->
+    morphism -> theory -> theory
+  val amend_registration: string * morphism -> morphism * bool ->
+    morphism -> theory -> theory
   val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
   val amend_registration_legacy: morphism -> string * morphism -> theory -> theory
   val add_dependency: string -> string * morphism -> morphism -> theory -> theory
@@ -474,7 +476,8 @@
         |> roundup thy add_reg export (name, base_morph)
         |> snd
         (* add mixin *)
-        |> amend_registration (name, base_morph) mixin export
+        |> (case mixin of NONE => I
+             | SOME mixin => amend_registration (name, base_morph) mixin export)
         (* activate import hierarchy as far as not already active *)
         |> Context.theory_map (activate_facts' export (name, base_morph))
       end