merged

--- a/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 12:25:56 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Wed Apr 24 12:26:28 2013 +0200
@@ -64,8 +64,7 @@
   unfolding shd_def stl_def stream_case_def stream_map_def stream.dtor_unfold
   by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor)
 
-lemma stream_map_Stream[simp, code]: "stream_map f (x ## s) = f x ## stream_map f s"
-  by (metis stream.exhaust stream.sels stream_map_simps)
+declare stream.map[code]
 
 theorem shd_stream_set: "shd s \<in> stream_set s"
   by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta)

--- a/src/HOL/Tools/case_translation.ML	Wed Apr 24 12:25:56 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 24 12:26:28 2013 +0200
@@ -156,7 +156,7 @@
 
 (* print translation *)
 
-fun case_tr' [_, x, t] =
+fun case_tr' (_ :: x :: t :: ts) =
       let
         fun mk_clause (Const (@{const_syntax case_abs}, _) $ Abs (s, T, t)) xs used =
               let val (s', used') = Name.variant s used
@@ -171,9 +171,9 @@
               mk_clause t [] (Term.declare_term_frees t Name.context) ::
               mk_clauses u
       in
-        Syntax.const @{syntax_const "_case_syntax"} $ x $
+        list_comb (Syntax.const @{syntax_const "_case_syntax"} $ x $
           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
-            (mk_clauses t)
+            (mk_clauses t), ts)
       end;
 
 val trfun_setup' = Sign.add_trfuns

--- a/src/Pure/Isar/expression.ML	Wed Apr 24 12:25:56 2013 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Apr 24 12:26:28 2013 +0200
@@ -829,7 +829,7 @@
 
 fun meta_rewrite eqns ctxt = (map (Local_Defs.meta_rewrite_rule ctxt #> Drule.abs_def) (maps snd eqns), ctxt);
 
-fun note_eqns_register note activate reinit deps witss eqns attrss export export' ctxt =
+fun note_eqns_register note activate deps witss eqns attrss export export' ctxt =
   let
     val facts = 
       (attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns);
@@ -843,22 +843,23 @@
   in
     ctxt'
     |> fold activate' dep_morphs
-    |> reinit
   end;
 
 fun generic_interpretation prep_expr parse_prop prep_attr setup_proof note add_registration
-    reinit expression raw_eqns initial_ctxt = 
+    expression raw_eqns initial_ctxt = 
   let
     val (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) = 
       read_interpretation prep_expr parse_prop prep_attr expression raw_eqns initial_ctxt;
     fun after_qed witss eqns =
-      note_eqns_register note add_registration reinit deps witss eqns attrss export export';
+      note_eqns_register note add_registration deps witss eqns attrss export export';
   in setup_proof after_qed propss eqns goal_ctxt end;
 
 val activate_proof = Context.proof_map ooo Locale.add_registration;
 val activate_local_theory = Local_Theory.target ooo activate_proof;
 val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-fun add_dependency locale = Local_Theory.raw_theory ooo Locale.add_dependency locale;
+fun add_dependency locale dep_morph mixin export =
+  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
+  #> activate_local_theory dep_morph mixin export;
 fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;
 
 fun gen_interpret prep_expr parse_prop prep_attr expression raw_eqns int state =
@@ -870,7 +871,7 @@
       Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret" propss eqns goal_ctxt int state;
   in
     generic_interpretation prep_expr parse_prop prep_attr setup_proof
-      Attrib.local_notes activate_proof I expression raw_eqns ctxt
+      Attrib.local_notes activate_proof expression raw_eqns ctxt
   end;
 
 fun gen_interpretation prep_expr parse_prop prep_attr expression raw_eqns lthy =
@@ -881,7 +882,7 @@
   in
     lthy
     |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind activate I expression raw_eqns
+        Local_Theory.notes_kind activate expression raw_eqns
   end;
 
 fun gen_sublocale prep_expr parse_prop prep_attr expression raw_eqns lthy =
@@ -893,7 +894,7 @@
   in
     lthy
     |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind (add_dependency locale) (Named_Target.reinit lthy) expression raw_eqns
+        Local_Theory.notes_kind (add_dependency locale) expression raw_eqns
   end;
   
 fun gen_sublocale_global prep_expr prep_loc parse_prop prep_attr before_exit raw_locale expression raw_eqns thy =
@@ -903,7 +904,7 @@
     thy
     |> Named_Target.init before_exit locale
     |> generic_interpretation prep_expr parse_prop prep_attr Element.witness_proof_eqs
-        Local_Theory.notes_kind (add_dependency_global locale) I expression raw_eqns
+        Local_Theory.notes_kind (add_dependency_global locale) expression raw_eqns
   end;
 
 in
@@ -916,11 +917,10 @@
         | NONE => error "Not in a named target";
     val is_theory = (target = "");
     val activate = if is_theory then add_registration else add_dependency target;
-    val reinit = if is_theory then I else Named_Target.reinit lthy;
   in
     lthy
     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
-        Local_Theory.notes_kind activate reinit expression raw_eqns
+        Local_Theory.notes_kind activate expression raw_eqns
   end;
 
 fun ephemeral_interpretation expression raw_eqns lthy =
@@ -932,7 +932,7 @@
     lthy
     |> Local_Theory.mark_brittle
     |> generic_interpretation cert_goal_expression (K I) (K I) Element.witness_proof_eqs
-        Local_Theory.notes_kind activate_local_theory I expression raw_eqns
+        Local_Theory.notes_kind activate_local_theory expression raw_eqns
   end;
 
 fun interpret x = gen_interpret cert_goal_expression (K I) (K I) x;