# HG changeset patch
# User wenzelm
# Date 1333389265 -7200
# Node ID 5e96bfb4a1594aa0a1ac23c1102ee791e9c9759d
# Parent  fc95b8b6c260e62cda61143979a781c41cc1a0ed
tuned;

diff -r fc95b8b6c260 -r 5e96bfb4a159 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Mon Apr 02 19:47:21 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Apr 02 19:54:25 2012 +0200
@@ -61,8 +61,8 @@
     val thy_ctxt = Proof_Context.init_global thy;
 
     (*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') = Thm.cterm_of thy rhs
+      |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
 
     val xs = Variable.add_fixed lthy rhs' [];
     val T = Term.fastype_of rhs;