Local_Defs.contract convenience;
authorwenzelm
Sat Mar 13 14:41:14 2010 +0100 (2010-03-13)
changeset 3573935a3b3721ffb
parent 35738 98fd035c3fe3
child 35740 d3726291f252
Local_Defs.contract convenience;
src/Pure/Isar/local_defs.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Sat Mar 13 14:40:36 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Sat Mar 13 14:41:14 2010 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
     1.5    val trans_terms: Proof.context -> thm list -> thm
     1.6    val trans_props: Proof.context -> thm list -> thm
     1.7 +  val contract: Proof.context -> thm list -> cterm -> thm -> thm
     1.8    val print_rules: Proof.context -> unit
     1.9    val defn_add: attribute
    1.10    val defn_del: attribute
    1.11 @@ -179,6 +180,8 @@
    1.12  
    1.13  end;
    1.14  
    1.15 +fun contract ctxt defs ct th =
    1.16 +  trans_props ctxt [th, Thm.symmetric (MetaSimplifier.rewrite true defs ct)];
    1.17  
    1.18  
    1.19  (** defived definitions **)
     2.1 --- a/src/Pure/Isar/theory_target.ML	Sat Mar 13 14:40:36 2010 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Mar 13 14:41:14 2010 +0100
     2.3 @@ -122,7 +122,6 @@
     2.4      (*export assumes/defines*)
     2.5      val th = Goal.norm_result raw_th;
     2.6      val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
     2.7 -    val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
     2.8      val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
     2.9      val nprems = Thm.nprems_of th' - Thm.nprems_of th;
    2.10  
    2.11 @@ -152,7 +151,7 @@
    2.12      val result'' =
    2.13        (case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
    2.14          NONE => raise THM ("Failed to re-import result", 0, [result'])
    2.15 -      | SOME res => Local_Defs.trans_props ctxt [res, Thm.symmetric concl_conv])
    2.16 +      | SOME res => Local_Defs.contract ctxt defs (Thm.cprop_of th) res)
    2.17        |> Goal.norm_result
    2.18        |> PureThy.name_thm false false name;
    2.19