--- 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;