# HG changeset patch
# User paulson
# Date 1141121390 -3600
# Node ID b294c097767ea43234ec7aaa0f974f8b7b91803d
# Parent  f48e36b7d8d4ab47b0f575fbc3457772cc3e5c43
new order for arity clauses

diff -r f48e36b7d8d4 -r b294c097767e src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Tue Feb 28 11:09:29 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Tue Feb 28 11:09:50 2006 +0100
@@ -700,19 +700,21 @@
 (** Isabelle arities **)
 
 fun arity_clause _ (tcons, []) = []
-  | arity_clause n (tcons, ("HOL.type",_)::ars) =  (*Should be ignored*)
+  | arity_clause n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
       arity_clause n (tcons,ars)
   | arity_clause n (tcons, ar::ars) =
       make_axiom_arity_clause (tcons,n,ar) :: 
       arity_clause (n+1) (tcons,ars);
 
 fun multi_arity_clause [] = []
-  | multi_arity_clause (tcon_ar :: tcons_ars)  =
-      arity_clause 0 tcon_ar  @  multi_arity_clause tcons_ars 
+  | multi_arity_clause ((tcons,ars) :: tc_arlists) =
+      (*Reversal ensures that older entries always get the same axiom name*)
+      arity_clause 0 (tcons, rev ars)  @  
+      multi_arity_clause tc_arlists 
 
 fun arity_clause_thy thy =
   let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy))
-  in multi_arity_clause (Symtab.dest arities) end;
+  in multi_arity_clause (rev (Symtab.dest arities)) end;
 
 
 (**** Find occurrences of predicates in clauses ****)
@@ -935,10 +937,10 @@
     val clss = conjectures @ axclauses
     val funcs = funcs_of_clauses clss arity_clauses
     and preds = preds_of_clauses clss classrel_clauses arity_clauses
-    val out = TextIO.openOut filename
     and probname = Path.pack (Path.base (Path.unpack filename))
     val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
     val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
+    val out = TextIO.openOut filename
   in
     TextIO.output (out, string_of_start probname); 
     TextIO.output (out, string_of_descrip probname);