# 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; (*