more basic Local_Defs.export_cterm;
authorwenzelm
Thu Mar 11 23:45:41 2010 +0100 (2010-03-11)
changeset 357171856c0172cf2
parent 35716 9dd4747d9591
child 35737 19eefc0655b6
more basic Local_Defs.export_cterm;
src/Pure/Isar/local_defs.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/local_defs.ML	Thu Mar 11 23:07:12 2010 +0100
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Thu Mar 11 23:45:41 2010 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4    val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     1.5      (term * term) * Proof.context
     1.6    val export: Proof.context -> Proof.context -> thm -> thm list * thm
     1.7 -  val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
     1.8 +  val export_cterm: Proof.context -> Proof.context -> cterm -> thm list * cterm
     1.9    val trans_terms: Proof.context -> thm list -> thm
    1.10    val trans_props: Proof.context -> thm list -> thm
    1.11    val print_rules: Proof.context -> unit
    1.12 @@ -155,8 +155,7 @@
    1.13       TERM b as          b xs == b as
    1.14  *)
    1.15  fun export_cterm inner outer ct =
    1.16 -  let val (defs, ct') = export inner outer (Drule.mk_term ct) ||> Drule.dest_term
    1.17 -  in (ct', MetaSimplifier.rewrite true defs ct) end;
    1.18 +  export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
    1.19  
    1.20  
    1.21  (* basic transitivity reasoning -- modulo beta-eta *)
     2.1 --- a/src/Pure/Isar/theory_target.ML	Thu Mar 11 23:07:12 2010 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Mar 11 23:45:41 2010 +0100
     2.3 @@ -278,8 +278,11 @@
     2.4      val thy_ctxt = ProofContext.init thy;
     2.5  
     2.6      val name' = Thm.def_binding_optional b name;
     2.7 -    val (rhs', rhs_conv) =
     2.8 -      Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
     2.9 +
    2.10 +    val crhs = Thm.cterm_of thy rhs;
    2.11 +    val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
    2.12 +    val rhs_conv = MetaSimplifier.rewrite true defs crhs;
    2.13 +
    2.14      val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
    2.15      val T = Term.fastype_of rhs;
    2.16