# HG changeset patch
# User wenzelm
# Date 1268487674 -3600
# Node ID 35a3b3721ffb9fb17c6c67ea3585da38ffbb3eb6
# Parent  98fd035c3fe309582f74c2d48b3d29909a07bb80
Local_Defs.contract convenience;

diff -r 98fd035c3fe3 -r 35a3b3721ffb src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 13 14:40:36 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 13 14:41:14 2010 +0100
@@ -20,6 +20,7 @@
   val export_cterm: Proof.context -> Proof.context -> cterm -> 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
   val print_rules: Proof.context -> unit
   val defn_add: attribute
   val defn_del: attribute
@@ -179,6 +180,8 @@
 
 end;
 
+fun contract ctxt defs ct th =
+  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
 
 
 (** defived definitions **)
diff -r 98fd035c3fe3 -r 35a3b3721ffb src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Mar 13 14:40:36 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Mar 13 14:41:14 2010 +0100
@@ -122,7 +122,6 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
-    val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
     val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
@@ -152,7 +151,7 @@
     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.trans_props ctxt [res, Thm.symmetric concl_conv])
+      | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
       |> Goal.norm_result
       |> PureThy.name_thm false false name;