# HG changeset patch
# User wenzelm
# Date 1320760991 -3600
# Node ID a83574606719a9b2b2342b17831d9854989bab1b
# Parent  b24ecaa46edb9830ee12279f1c4997028cba895f
more specific treatment of defines/assumes -- avoid normalizing defs by themselves (NB: locale specifications and Local_Theory.define may lead to arbitrary mixture);

diff -r b24ecaa46edb -r a83574606719 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Nov 08 12:20:26 2011 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Nov 08 15:03:11 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 b24ecaa46edb -r a83574606719 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Nov 08 12:20:26 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Tue Nov 08 15:03:11 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 b24ecaa46edb -r a83574606719 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Nov 08 12:20:26 2011 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Nov 08 15:03:11 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
@@ -138,19 +138,22 @@
     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 defs = prems |> filter (fn prem =>
-        (case try (head_of_def o Thm.prop_of) prem of
-          SOME x =>
-            let val t = Free x in
-              (case try exp_term t of
-                SOME u => not (t aconv u)
-              | NONE => false)
-            end
-        | NONE => false));
-    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;
 
 (*