# HG changeset patch
# User paulson
# Date 1169023974 -3600
# Node ID b161604f0c8d5af1ae3c0f53bcaebd1786c5dcc4
# Parent  5084f53cef39801c17d8fe17bc872fd7f2577967
Deleted mk_fol_type, since the constructors can be used directly

diff -r 5084f53cef39 -r b161604f0c8d src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Wed Jan 17 09:52:06 2007 +0100
+++ b/src/HOL/Tools/res_clause.ML	Wed Jan 17 09:52:54 2007 +0100
@@ -48,7 +48,6 @@
   val make_schematic_type_var : string * int -> string
   val make_schematic_var : string * int -> string
   val make_type_class : string -> string
-  val mk_fol_type: string * string * fol_type list -> fol_type
   val mk_typ_var_sort : Term.typ -> typ_var * sort
   val paren_pack : string list -> string
   val schematic_var_prefix : string
@@ -222,11 +221,6 @@
   | string_of_fol_type (Comp(tcon,tps)) = 
       tcon ^ (paren_pack (map string_of_fol_type tps));
       
-fun mk_fol_type ("Var",x,_) = AtomV(x)
-  | mk_fol_type ("Fixed",x,_) = AtomF(x)
-  | mk_fol_type ("Comp",con,args) = Comp(con,args)
-
-
 (*First string is the type class; the second is a TVar or TFfree*)
 datatype type_literal = LTVar of string * string | LTFree of string * string;