src/HOL/Tools/res_clause.ML
changeset 22079 b161604f0c8d
parent 21858 05f57309170c
child 22130 0906fd95e0b5
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jan 17 09:52:06 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Jan 17 09:52:54 2007 +0100
     1.3 @@ -48,7 +48,6 @@
     1.4    val make_schematic_type_var : string * int -> string
     1.5    val make_schematic_var : string * int -> string
     1.6    val make_type_class : string -> string
     1.7 -  val mk_fol_type: string * string * fol_type list -> fol_type
     1.8    val mk_typ_var_sort : Term.typ -> typ_var * sort
     1.9    val paren_pack : string list -> string
    1.10    val schematic_var_prefix : string
    1.11 @@ -222,11 +221,6 @@
    1.12    | string_of_fol_type (Comp(tcon,tps)) = 
    1.13        tcon ^ (paren_pack (map string_of_fol_type tps));
    1.14        
    1.15 -fun mk_fol_type ("Var",x,_) = AtomV(x)
    1.16 -  | mk_fol_type ("Fixed",x,_) = AtomF(x)
    1.17 -  | mk_fol_type ("Comp",con,args) = Comp(con,args)
    1.18 -
    1.19 -
    1.20  (*First string is the type class; the second is a TVar or TFfree*)
    1.21  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.22