# HG changeset patch
# User paulson
# Date 1166010146 -3600
# Node ID 06a06f6d3166eeb2e24d513221df2cebe3db70f4
# Parent  2776dcfd5617b178bd15efd026d4ac6f0f48fe70
Deleted the unused type argument of UVar

diff -r 2776dcfd5617 -r 06a06f6d3166 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Dec 13 12:10:54 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML	Wed Dec 13 12:42:26 2006 +0100
@@ -14,7 +14,7 @@
   datatype fol_type = AtomV of string
                     | AtomF of string
                     | Comp of string * fol_type list;
-  datatype fol_term = UVar of string * fol_type
+  datatype fol_term = UVar of string
                     | Fun of string * fol_type list * fol_term list;
   datatype predicate = Predicate of string * fol_type list * fol_term list;
   datatype kind = Axiom | Conjecture;
@@ -55,13 +55,13 @@
   val string_of_fol_type : fol_type -> string
   val tconst_prefix : string 
   val tfree_prefix : string
+  val tvar_prefix : string
   val tptp_arity_clause : arityClause -> string
   val tptp_classrelClause : classrelClause -> string
   val tptp_of_typeLit : type_literal -> string
   val tptp_tfree_clause : string -> string
   val tptp_write_file: thm list -> string -> 
        ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
-  val tvar_prefix : string
   val union_all : ''a list list -> ''a list
   val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
   val dfg_sign: bool -> string -> string
@@ -230,7 +230,7 @@
 (*First string is the type class; the second is a TVar or TFfree*)
 datatype type_literal = LTVar of string * string | LTFree of string * string;
 
-datatype fol_term = UVar of string * fol_type
+datatype fol_term = UVar of string
                   | Fun of string * fol_type list * fol_term list;
 datatype predicate = Predicate of string * fol_type list * fol_term list;
 
@@ -304,14 +304,6 @@
   | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
   | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
 
-
-(* For typed equality *)
-(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
-(* Find type of equality arg *)
-fun eq_arg_type (Type("fun",[T,_])) = 
-    let val (folT,_) = type_of T;
-    in  folT  end;
-
 fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T))
   | fun_name_type (Free(x,T)) args  = 
        if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T))
@@ -321,13 +313,13 @@
 (*Convert a term to a fol_term while accumulating sort constraints on the TFrees and
   TVars it contains.*)    
 fun term_of (Var(ind_nm,T)) = 
-      let val (folType,ts) = type_of T
-      in (UVar(make_schematic_var ind_nm, folType), ts) end
+      let val (_,ts) = type_of T
+      in (UVar(make_schematic_var ind_nm), ts) end
   | term_of (Free(x,T)) = 
-      let val (folType, ts) = type_of T
+      let val (_,ts) = type_of T
       in
-	  if isMeta x then (UVar(make_schematic_var(x,0),folType), ts)
-	  else (Fun(make_fixed_var x, [], []), ts)  (*Frees don't need types!*)
+	  if isMeta x then (UVar(make_schematic_var(x,0)), ts)
+	  else (Fun(make_fixed_var x, [], []), ts)
       end
   | term_of app = 
       let val (f,args) = strip_comb app
@@ -340,11 +332,9 @@
 
 (*Create a predicate value, again accumulating sort constraints.*)    
 fun pred_of (Const("op =", typ), args) =
-      let val arg_typ = eq_arg_type typ 
-	  val (args',ts) = terms_of args
-	  val equal_name = make_fixed_const "op ="
+      let val (args',ts) = terms_of args
       in
-	  (Predicate(equal_name,[arg_typ],args'),
+	  (Predicate(make_fixed_const "op =", [], args'),
 	   union_all ts)
       end
   | pred_of (pred,args) = 
@@ -595,7 +585,7 @@
   | add_foltype_funcs (Comp(a,tys), funcs) = 
       foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
 
-fun add_folterm_funcs (UVar(_,ty), funcs) = add_foltype_funcs (ty, funcs)
+fun add_folterm_funcs (UVar _, funcs) = funcs
   | add_folterm_funcs (Fun(a,tys,tms), funcs) = 
       foldl add_foltype_funcs 
 	    (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 
@@ -629,7 +619,7 @@
 
 (**** String-oriented operations ****)
 
-fun string_of_term (UVar(x,_)) = x
+fun string_of_term (UVar x) = x
   | string_of_term (Fun (name,typs,terms)) = 
       name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs));
 
@@ -688,7 +678,7 @@
   let val Predicate (_, _, folterms) = pred
   in  folterms  end
 
-fun get_uvars (UVar(a,typ)) = [a] 
+fun get_uvars (UVar a) = [a] 
   | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
 
 fun dfg_vars (Clause {literals,...}) =