# HG changeset patch
# User wenzelm
# Date 1139534544 -3600
# Node ID 910fbe64033c3e4ad148ec8d04a6655fbdbb9855
# Parent  0ded3b84287827e71326e41e7c2f409d6ee3e753
abbrevs: store in reverted orientation;
tuned;

diff -r 0ded3b842878 -r 910fbe64033c src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Feb 10 02:22:23 2006 +0100
+++ b/src/Pure/consts.ML	Fri Feb 10 02:22:24 2006 +0100
@@ -22,7 +22,7 @@
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: NameSpace.naming -> bstring * typ -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> bool -> string * term -> T -> T
+  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> bool -> bstring * term -> T -> T
   val constrain: string * typ -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
@@ -166,7 +166,7 @@
   let
     val (xs, body) = Term.strip_abs (Envir.beta_eta_contract rhs);
     val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) [];
-  in (Term.list_comb (Const const, vars), Term.subst_bounds (rev vars, body)) end;
+  in (Term.subst_bounds (rev vars, body), Term.list_comb (Const const, vars)) end;
 
 fun abbreviate pp tsig naming revert (c, raw_rhs) consts =
     consts |> map_consts (fn (decls, abbrevs, constraints) =>