# HG changeset patch
# User blanchet
# Date 1306485007 -7200
# Node ID 5a86009366fcb42e695524a0173f51dbc8dd73c7
# Parent  e88fde86e4c23b3a78df64f5ff733770e9ba2cbc
tuning

diff -r e88fde86e4c2 -r 5a86009366fc src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Fri May 27 10:30:07 2011 +0200
@@ -25,7 +25,7 @@
   datatype class_rel_clause =
     ClassRelClause of {name: string, subclass: name, superclass: name}
   datatype combterm =
-    CombConst of name * typ * typ list (* Const and Free *) |
+    CombConst of name * typ * typ list |
     CombVar of name * typ |
     CombApp of combterm * combterm
   datatype fol_literal = FOLLiteral of bool * combterm
@@ -371,9 +371,8 @@
           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
       in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
 
-fun make_arity_clauses thy tycons classes =
-  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
-  in  (classes', multi_arity_clause cpairs)  end;
+fun make_arity_clauses thy tycons =
+  iter_type_class_pairs thy tycons ##> multi_arity_clause
 
 datatype combterm =
   CombConst of name * typ * typ list (* Const and Free *) |
@@ -518,11 +517,11 @@
 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
 fun add_type_consts_in_term thy =
   let
-    fun aux (Const x) =
+    fun aux (Const (@{const_name Meson.skolem}, _) $ _) = I
+      | aux (t $ u) = aux t #> aux u
+      | aux (Const x) =
         fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
       | aux (Abs (_, _, u)) = aux u
-      | aux (Const (@{const_name Meson.skolem}, _) $ _) = I
-      | aux (t $ u) = aux t #> aux u
       | aux _ = I
   in aux end
 
@@ -740,7 +739,7 @@
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
       val supers = tvar_classes_of_terms tms
-      and tycons = type_consts_of_terms thy tms
+      val tycons = type_consts_of_terms thy tms
       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
       val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses