# HG changeset patch
# User wenzelm
# Date 1268347541 -3600
# Node ID 1856c0172cf21131803b19b23e4df492a5db783e
# Parent  9dd4747d95916386229c55cc95c26a0efdc3cd5c
more basic Local_Defs.export_cterm;

diff -r 9dd4747d9591 -r 1856c0172cf2 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Thu Mar 11 23:07:12 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML	Thu Mar 11 23:45:41 2010 +0100
@@ -17,7 +17,7 @@
   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 -> cterm * thm
+  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 print_rules: Proof.context -> unit
@@ -155,8 +155,7 @@
      TERM b as          b xs == b as
 *)
 fun export_cterm inner outer ct =
-  let val (defs, ct') = export inner outer (Drule.mk_term ct) ||> Drule.dest_term
-  in (ct', MetaSimplifier.rewrite true defs ct) end;
+  export inner outer (Drule.mk_term ct) ||> Drule.dest_term;
 
 
 (* basic transitivity reasoning -- modulo beta-eta *)
diff -r 9dd4747d9591 -r 1856c0172cf2 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Mar 11 23:07:12 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 11 23:45:41 2010 +0100
@@ -278,8 +278,11 @@
     val thy_ctxt = ProofContext.init thy;
 
     val name' = Thm.def_binding_optional b name;
-    val (rhs', rhs_conv) =
-      Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
+
+    val crhs = Thm.cterm_of thy rhs;
+    val (defs, rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
+    val rhs_conv = MetaSimplifier.rewrite true defs crhs;
+
     val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
     val T = Term.fastype_of rhs;