src/HOL/Tools/ATP/reduce_axiomsN.ML
changeset 19035 678ef6658a0e
parent 19009 bb29bf9d3a72
child 19200 1da6b9a1575d
equal deleted inserted replaced
19034:db16746a5604 19035:678ef6658a0e
   230 
   230 
   231 
   231 
   232 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
   232 fun uni_constants (c1,ctp1) (c2,ctp2) = (c1 = c2) andalso (uni_types ctp1 ctp2);
   233 
   233 
   234 fun uni_mem _ [] = false
   234 fun uni_mem _ [] = false
   235   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c,c_typ) (c1,c_typ1)) orelse (uni_mem (c,c_typ) ctyps);
   235   | uni_mem (c,c_typ) ((c1,c_typ1)::ctyps) = (uni_constants (c1,c_typ1) (c,c_typ)) orelse (uni_mem (c,c_typ) ctyps);
   236 
   236 
   237 
   237 
   238 
   238 
   239 fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
   239 fun const_typ_of (Type (c,typs)) = CType (c,map const_typ_of typs) 
   240   | const_typ_of (TFree(_,_)) = CTVar
   240   | const_typ_of (TFree(_,_)) = CTVar