# HG changeset patch
# User wenzelm
# Date 1320770842 -3600
# Node ID af607f4945f4109af7e01e278cd2954f286ef2ed
# Parent  d58c25559dc00747840d9dafcd0bb6073106ca4b# Parent  a83574606719a9b2b2342b17831d9854989bab1b
merged

diff -r d58c25559dc0 -r af607f4945f4 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Library/reflection.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -60,10 +60,11 @@
    fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
      | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
    fun tryext x = (x RS ext2 handle THM _ =>  x)
-   val cong = (Goal.prove ctxt'' [] (map mk_def env)
-                          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
-                          (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
-                                                        THEN rtac th' 1)) RS sym
+   val cong =
+    (Goal.prove ctxt'' [] (map mk_def env)
+      (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
+      (fn {context, prems, ...} =>
+        Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym
 
    val (cong' :: vars') =
        Variable.export ctxt'' ctxt (cong :: map (Drule.mk_term o cert) vs)
diff -r d58c25559dc0 -r af607f4945f4 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -176,7 +176,7 @@
   end
 
 fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
-  import (export : thm -> thm) sum_psimp_eq =
+    import (export : thm -> thm) sum_psimp_eq =
   let
     val (MutualPart {f=SOME f, ...}) = get_part fname parts
 
@@ -190,9 +190,10 @@
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
-         THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
+      (fn _ =>
+        Local_Defs.unfold_tac ctxt all_orig_fdefs
+          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
+          THEN (simp_tac (simpset_of ctxt)) 1)
     |> restore_cond
     |> export
   end
diff -r d58c25559dc0 -r af607f4945f4 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -64,7 +64,7 @@
 
 (*rewrite conclusion with k-th assumtion*)
 fun rewrite_with_asm_tac ctxt k =
-  Subgoal.FOCUS (fn {context=ctxt', prems, ...} =>
+  Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
     Local_Defs.unfold_tac ctxt' [nth prems k]) ctxt;
 
 fun dest_case thy t =
diff -r d58c25559dc0 -r af607f4945f4 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -183,7 +183,7 @@
       let
         val thy = Proof_Context.theory_of set_lthy;
         val cert = Thm.cterm_of thy;
-        val (defs, A) =
+        val ((defs, _), A) =
           Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
           ||> Thm.term_of;
 
diff -r d58c25559dc0 -r af607f4945f4 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -57,7 +57,7 @@
 
     (*term and type parameters*)
     val crhs = Thm.cterm_of thy rhs;
-    val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
+    val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
     val rhs_conv = Raw_Simplifier.rewrite true defs crhs;
 
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
@@ -105,11 +105,8 @@
 
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
-    val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
-    val assms =
-      map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
-        (Assumption.all_assms_of ctxt);
-    val nprems = Thm.nprems_of th' - Thm.nprems_of th;
+    val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
+    val asms' = map (Raw_Simplifier.rewrite_rule defs) asms;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
@@ -134,11 +131,10 @@
     val result' = Thm.instantiate (cinstT, cinst) result;
 
     (*import assumes/defines*)
-    val assm_tac = FIRST' (map (fn assm => Tactic.compose_tac (false, assm, 0)) assms);
     val result'' =
-      (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
-        NONE => raise THM ("Failed to re-import result", 0, [result'])
-      | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
+      (fold (curry op COMP) asms' result'
+        handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
+      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
       |> Goal.norm_result
       |> Global_Theory.name_thm false false name;
 
diff -r d58c25559dc0 -r af607f4945f4 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -15,8 +15,8 @@
   val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
-  val export: Proof.context -> Proof.context -> thm -> thm list * thm
-  val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
+  val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
+  val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm
   val trans_terms: Proof.context -> thm list -> thm
   val trans_props: Proof.context -> thm list -> thm
   val contract: Proof.context -> thm list -> cterm -> thm -> thm
@@ -66,7 +66,7 @@
 (* export defs *)
 
 val head_of_def =
-  #1 o Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
+  Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body;
 
 
 (*
@@ -78,7 +78,7 @@
 *)
 fun expand defs =
   Drule.implies_intr_list defs
-  #> Drule.generalize ([], map (head_of_def o Thm.term_of) defs)
+  #> Drule.generalize ([], map (#1 o head_of_def o Thm.term_of) defs)
   #> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
@@ -136,16 +136,24 @@
 fun export inner outer =    (*beware of closure sizes*)
   let
     val exp = Assumption.export false inner outer;
+    val exp_term = Assumption.export_term inner outer;
     val prems = Assumption.all_prems_of inner;
-  in fn th =>
-    let
-      val th' = exp th;
-      val still_fixed = map #1 (Thm.fold_terms Term.add_frees th' []);
-      val defs = prems |> filter_out (fn prem =>
-        (case try (head_of_def o Thm.prop_of) prem of
-          SOME x => member (op =) still_fixed x
-        | NONE => true));
-    in (map Drule.abs_def defs, th') end
+  in
+    fn th =>
+      let
+        val th' = exp th;
+        val defs_asms = prems |> map (fn prem =>
+          (case try (head_of_def o Thm.prop_of) prem of
+            NONE => (prem, false)
+          | SOME x =>
+              let val t = Free x in
+                (case try exp_term t of
+                  NONE => (prem, false)
+                | SOME u =>
+                    if t aconv u then (prem, false)
+                    else (Drule.abs_def prem, true))
+              end));
+      in (pairself (map #1) (List.partition #2 defs_asms), th') end
   end;
 
 (*
diff -r d58c25559dc0 -r af607f4945f4 src/Pure/net.ML
--- a/src/Pure/net.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/net.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -54,7 +54,7 @@
         | rands (Const(c,_), cs) = AtomK c :: cs
         | rands (Free(c,_),  cs) = AtomK c :: cs
         | rands (Bound i,  cs)   = AtomK (Name.bound i) :: cs
-  in case (head_of t) of
+  in case head_of t of
       Var _ => VarK :: cs
     | Abs _ => VarK :: cs
     | _     => rands(t,cs)
@@ -103,9 +103,7 @@
         | ins1 (VarK :: keys, Net{comb,var,atoms}) =
             Net{comb=comb, var=ins1(keys,var), atoms=atoms}
         | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
-            let
-              val net' = the_default empty (Symtab.lookup atoms a);
-              val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
+            let val atoms' = Symtab.map_default (a, empty) (fn net' => ins1 (keys, net')) atoms;
             in  Net{comb=comb, var=var, atoms=atoms'}  end
   in  ins1 (keys,net)  end;
 
diff -r d58c25559dc0 -r af607f4945f4 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Nov 08 14:29:24 2011 +0100
+++ b/src/Pure/raw_simplifier.ML	Tue Nov 08 17:47:22 2011 +0100
@@ -456,7 +456,6 @@
     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
       raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
-    val elhs = if term_of elhs aconv term_of lhs then lhs else elhs;  (*share identical copies*)
     val erhs = Envir.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso