rename "combtyp" constructors

--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Wed Jul 21 21:14:26 2010 +0200
@@ -21,9 +21,9 @@
   datatype classrel_clause = ClassrelClause of
    {axiom_name: string, subclass: name, superclass: name}
   datatype combtyp =
-    TyVar of name |
-    TyFree of name |
-    TyConstr of name * combtyp list
+    CombTVar of name |
+    CombTFree of name |
+    CombType of name * combtyp list
   datatype combterm =
     CombConst of name * combtyp * combtyp list (* Const and Free *) |
     CombVar of name * combtyp |
@@ -352,9 +352,9 @@
   in  (classes', multi_arity_clause cpairs)  end;
 
 datatype combtyp =
-  TyVar of name |
-  TyFree of name |
-  TyConstr of name * combtyp list
+  CombTVar of name |
+  CombTFree of name |
+  CombType of name * combtyp list
 
 datatype combterm =
   CombConst of name * combtyp * combtyp list (* Const and Free *) |
@@ -372,7 +372,7 @@
 (*********************************************************************)
 
 (*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
+fun result_type (CombType (_, [_, tp2])) = tp2
   | result_type _ = raise Fail "non-function type"
 
 fun type_of_combterm (CombConst (_, tp, _)) = tp
@@ -387,11 +387,11 @@
 
 fun type_of (Type (a, Ts)) =
     let val (folTypes,ts) = types_of Ts in
-      (TyConstr (`make_fixed_type_const a, folTypes), ts)
+      (CombType (`make_fixed_type_const a, folTypes), ts)
     end
-  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+  | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
   | type_of (tp as TVar (x, _)) =
-    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
+    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
 and types_of Ts =
     let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
       (folTyps, union_all ts)
@@ -399,10 +399,10 @@
 
 (* same as above, but no gathering of sort information *)
 fun simp_type_of (Type (a, Ts)) =
-      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
-  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+      CombType (`make_fixed_type_const a, map simp_type_of Ts)
+  | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
   | simp_type_of (TVar (x, _)) =
-    TyVar (make_schematic_type_var x, string_of_indexname x)
+    CombTVar (make_schematic_type_var x, string_of_indexname x)
 
 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
 fun combterm_of thy (Const (c, T)) =

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jul 21 21:14:26 2010 +0200
@@ -70,9 +70,9 @@
 
 fun metis_lit b c args = (b, (c, args));
 
-fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
-  | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
-  | hol_type_to_fol (TyConstr ((s, _), tps)) =
+fun hol_type_to_fol (CombTVar (x, _)) = Metis.Term.Var x
+  | hol_type_to_fol (CombTFree (s, _)) = Metis.Term.Fn (s, [])
+  | hol_type_to_fol (CombType ((s, _), tps)) =
     Metis.Term.Fn (s, map hol_type_to_fol tps);
 
 (*These two functions insert type literals before the real literals. That is the

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:07 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jul 21 21:14:26 2010 +0200
@@ -120,9 +120,9 @@
 
 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
 
-fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
-  | atp_term_for_combtyp (TyFree name) = ATerm (name, [])
-  | atp_term_for_combtyp (TyConstr (name, tys)) =
+fun atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
+  | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
+  | atp_term_for_combtyp (CombType (name, tys)) =
     ATerm (name, map atp_term_for_combtyp tys)
 
 fun atp_term_for_combterm full_types top_level u =