equal
deleted
inserted
replaced
115 let |
115 let |
116 fun msg trm = |
116 fun msg trm = |
117 let |
117 let |
118 val hd = head_of trm |
118 val hd = head_of trm |
119 in |
119 in |
120 if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then () |
120 if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then () |
121 else (if strict_flag then error else warning) |
121 else (if strict_flag then error else warning) |
122 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
122 ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm)) |
123 end |
123 end |
124 |
124 |
125 val _ = case (term_of ctrm) of |
125 val _ = case (term_of ctrm) of |