1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Mar 18 14:31:50 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Mar 22 16:30:43 2005 +0100
     1.3 @@ -239,11 +239,24 @@
     1.4    | pred_name_type (Var(_,_))   = raise CLAUSE("Predicate Not First Order")
     1.5    | pred_name_type _          = raise CLAUSE("Predicate input unexpected");
     1.6  
     1.7 +
     1.8 +(* For type equality *)
     1.9 +(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
    1.10 +(* Find type of equality arg *)
    1.11 +fun eq_arg_type (Type("fun",[T,_])) = 
    1.12 +    let val (folT,_) = type_of T;
    1.13 +    in
    1.14 +	folT
    1.15 +    end;
    1.16 +
    1.17 +
    1.18 +
    1.19  fun fun_name_type (Const(c,T)) = (lookup_const c,type_of T)
    1.20    | fun_name_type (Free(x,T)) = (make_fixed_var x,type_of T)
    1.21    | fun_name_type _ = raise CLAUSE("Function Not First Order");
    1.22      
    1.23  
    1.24 +
    1.25  fun term_of (Var(ind_nm,T)) = 
    1.26      let val (folType,ts) = type_of T
    1.27      in
    1.28 @@ -257,7 +270,7 @@
    1.29  	else
    1.30              (Fun(make_fixed_var x,folType,[]),ts)
    1.31      end
    1.32 -  | term_of (Const(c,T)) = 
    1.33 +  | term_of (Const(c,T)) =  (* impossible to be equality *)
    1.34      let val (folType,ts) = type_of T
    1.35       in
    1.36          (Fun(lookup_const c,folType,[]),ts)
    1.37 @@ -271,8 +284,16 @@
    1.38              in
    1.39  		(Fun(funName,funType,args'),ts3)
    1.40              end
    1.41 +	fun term_of_eq ((Const ("op =", typ)),args) =
    1.42 +	    let val arg_typ = eq_arg_type typ
    1.43 +		val (args',ts) = ResLib.unzip (map term_of args)
    1.44 +		val equal_name = lookup_const ("op =")
    1.45 +	    in
    1.46 +		(Fun(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
    1.47 +	    end
    1.48      in
    1.49 -        case f of Const(_,_) => term_of_aux ()
    1.50 +        case f of Const ("op =", typ) => term_of_eq (f,args)
    1.51 +	        | Const(_,_) => term_of_aux ()
    1.52                  | Free(s,_)  => if (checkMeta s) then (raise CLAUSE("Function Not First Order")) else term_of_aux ()
    1.53                  | _          => raise CLAUSE("Function Not First Order")
    1.54      end
    1.55 @@ -281,19 +302,6 @@
    1.56  
    1.57  
    1.58  
    1.59 -(* For type equality *)
    1.60 -(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
    1.61 -(* Find type of equality arg *)
    1.62 -local
    1.63 -
    1.64 -fun eq_arg_type (Type("fun",[T,_])) = 
    1.65 -    let val (folT,_) = type_of T;
    1.66 -    in
    1.67 -	folT
    1.68 -    end;
    1.69 -
    1.70 -in
    1.71 -
    1.72  fun pred_of_eq ((Const ("op =", typ)),args) =
    1.73      let val arg_typ = eq_arg_type typ 
    1.74  	val (args',ts) = ResLib.unzip (map term_of args)
    1.75 @@ -302,7 +310,6 @@
    1.76  	(Predicate(equal_name,arg_typ,args'),ResLib.flat_noDup ts)
    1.77      end;
    1.78  
    1.79 -end;
    1.80  
    1.81  (* changed for non-equality predicate *)
    1.82  (* The input "pred" cannot be an equality *)
    1.83 @@ -553,17 +560,6 @@
    1.84  
    1.85  fun string_of_axiomName (Clause cls) = #axiom_name cls;
    1.86  
    1.87 -fun string_of_term (UVar(x,_)) = x
    1.88 -  | string_of_term (Fun (name,typ,[])) = name
    1.89 -  | string_of_term (Fun (name,typ,terms)) = 
    1.90 -    let val terms' = map string_of_term terms
    1.91 -    in
    1.92 -        if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms'))
    1.93 -        else name ^ (ResLib.list_to_string terms')
    1.94 -    end;
    1.95 -
    1.96 -
    1.97 -
    1.98  (****!!!! Changed for typed equality !!!!****)
    1.99  fun wrap_eq_type typ t = eq_typ_wrapper ^"(" ^ t ^ "," ^ typ ^ ")";
   1.100  
   1.101 @@ -577,6 +573,18 @@
   1.102  	    "equal(" ^ (wrap_eq_type typ tstr1) ^ "," ^ (wrap_eq_type typ tstr2) ^ ")"
   1.103  	else
   1.104  	    "equal(" ^ tstr1 ^ "," ^ tstr2 ^ ")"
   1.105 +    end
   1.106 +
   1.107 +
   1.108 +and
   1.109 +    string_of_term (UVar(x,_)) = x
   1.110 +  | string_of_term (Fun("equal",typ,terms)) = string_of_equality(typ,terms)
   1.111 +  | string_of_term (Fun (name,typ,[])) = name
   1.112 +  | string_of_term (Fun (name,typ,terms)) = 
   1.113 +    let val terms' = map string_of_term terms
   1.114 +    in
   1.115 +        if (!keep_types) then name ^ (ResLib.list_to_string (typ :: terms'))
   1.116 +        else name ^ (ResLib.list_to_string terms')
   1.117      end;
   1.118  
   1.119