src/HOL/Tools/inductive_set.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33049 c38f02fdf35d
equal deleted inserted replaced
33037:b22e44496dc2 33038:8f9594c31de4
   207            handle Subscript => error "infer_arities: bad term")
   207            handle Subscript => error "infer_arities: bad term")
   208     | _ => fold (infer_arities thy arities) (map (pair NONE) ts)
   208     | _ => fold (infer_arities thy arities) (map (pair NONE) ts)
   209       (case optf of
   209       (case optf of
   210          NONE => fs
   210          NONE => fs
   211        | SOME f => AList.update op = (u, the_default f
   211        | SOME f => AList.update op = (u, the_default f
   212            (Option.map (curry (gen_inter (op =)) f) (AList.lookup op = fs u))) fs));
   212            (Option.map (curry (inter (op =)) f) (AList.lookup op = fs u))) fs));
   213 
   213 
   214 
   214 
   215 (**************************************************************)
   215 (**************************************************************)
   216 (*    derive the to_pred equation from the to_set equation    *)
   216 (*    derive the to_pred equation from the to_set equation    *)
   217 (*                                                            *)
   217 (*                                                            *)