src/HOL/Tools/Sledgehammer/metis_clauses.ML

   datatype arity_clause = ArityClause of
    {axiom_name: string, conclLit: arLit, premLits: arLit list}
   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 |
     CombApp of combterm * combterm
   datatype fol_literal = FOLLiteral of bool * combterm

 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;
 
 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 |
   CombApp of combterm * combterm

 (*********************************************************************)
 (* convert a clause with type Term.term to a clause with type clause *)
 (*********************************************************************)
 
 (*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
   | type_of_combterm (CombVar (_, tp)) = tp
   | type_of_combterm (CombApp (t1, _)) = result_type (type_of_combterm t1)

         |   stripc  x =  x
     in stripc(u,[]) end
 
 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)
     end
 
 (* 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)) =
       let
         val (tp, ts) = type_of T