merged

--- a/src/HOL/Quotient.thy	Tue Aug 10 16:03:54 2010 +0200
+++ b/src/HOL/Quotient.thy	Wed Aug 11 08:50:20 2010 +0200
@@ -136,16 +136,6 @@
   shows "((op =) ===> (op =)) = (op =)"
   by (simp add: expand_fun_eq)
 
-lemma fun_rel_id:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-  using a by simp
-
-lemma fun_rel_id_asm:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
-  shows "A \<longrightarrow> (R1 ===> R2) f g"
-  using a by auto
-
 
 subsection {* Quotient Predicate *}
 
@@ -597,7 +587,7 @@
 lemma quot_rel_rsp:
   assumes a: "Quotient R Abs Rep"
   shows "(R ===> R ===> op =) R R"
-  apply(rule fun_rel_id)+
+  apply(rule fun_relI)+
   apply(rule equals_rsp[OF a])
   apply(assumption)+
   done

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Aug 10 16:03:54 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Aug 11 08:50:20 2010 +0200
@@ -316,7 +316,7 @@
    The deterministic part:
     - remove lambdas from both sides
     - prove Ball/Bex/Babs equalities using ball_rsp, bex_rsp, babs_rsp
-    - prove Ball/Bex relations unfolding fun_rel_id
+    - prove Ball/Bex relations using fun_relI
     - reflexivity of equality
     - prove equality of relations using equals_rsp
     - use user-supplied RSP theorems
@@ -335,7 +335,7 @@
 (case (bare_concl goal) of
     (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *)
   (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *)
 | (Const (@{const_name "op ="},_) $
@@ -347,7 +347,7 @@
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *)
 | Const (@{const_name "op ="},_) $
@@ -359,7 +359,7 @@
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
-      => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
+      => rtac @{thm fun_relI} THEN' quot_true_tac ctxt unlam
 
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
     (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)

--- a/src/Pure/Isar/expression.ML	Tue Aug 10 16:03:54 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 11 08:50:20 2010 +0200
@@ -451,7 +451,7 @@
     (* Declare parameters and imported facts *)
     val context' = context |>
       fix_params fixed |>
-      fold Locale.activate_declarations deps;
+      fold (Context.proof_map o Locale.activate_facts NONE) deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
       fold_map activate elems;

--- a/src/Pure/Isar/locale.ML	Tue Aug 10 16:03:54 2010 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 11 08:50:20 2010 +0200
@@ -53,7 +53,7 @@
 
   (* Activation *)
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
-  val activate_facts: morphism -> string * morphism -> Context.generic -> Context.generic
+  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
@@ -422,8 +422,12 @@
 fun activate_facts export dep context =
   let
     val thy = Context.theory_of context;
-    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context (SOME export);
-  in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
+    val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
+  in
+    roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
+      dep (get_idents context, context)
+    |-> put_idents
+  end;
 
 fun init name thy =
   activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
@@ -468,7 +472,7 @@
       |> (case mixin of NONE => I
            | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
-      |> activate_facts export (name, morph)
+      |> activate_facts (SOME export) (name, morph)
   end;