# HG changeset patch
# User wenzelm
# Date 1333456636 -7200
# Node ID ba9c8613ad9bd8774625fd6a5e9b4bd200474535
# Parent  323b7d74b2a83768362ab0bc6ca891c751e67f25
more uniform abbrev vs. define;

diff -r 323b7d74b2a8 -r ba9c8613ad9b src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 13:47:15 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 14:37:16 2012 +0200
@@ -188,18 +188,15 @@
 fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
-    val target_ctxt = Local_Theory.target_of lthy;
 
-    val t' = Assumption.export_term lthy target_ctxt t;
-    val xs = map Free (rev (Variable.add_fixed lthy t' []));
+    val t' = Assumption.export_term lthy thy_ctxt t;
+    val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
     val u = fold_rev lambda xs t';
+    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
 
     val extra_tfrees =
       subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
-
-    val global_rhs =
-      singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   in
     lthy
     |> target_abbrev prmode (b, mx') (global_rhs, t') xs