equal
deleted
inserted
replaced
145 handle TERM _ => err "Not a meta-equality (==)"; |
145 handle TERM _ => err "Not a meta-equality (==)"; |
146 val (head, args) = strip_comb lhs; |
146 val (head, args) = strip_comb lhs; |
147 val (c, ty) = dest_Const head |
147 val (c, ty) = dest_Const head |
148 handle TERM _ => err "Head of lhs not a constant"; |
148 handle TERM _ => err "Head of lhs not a constant"; |
149 |
149 |
150 fun occs_const (Const (c', _)) = (c = c') |
150 fun occs_const (Const c_ty') = (c_ty' = (c, ty)) |
151 | occs_const (Abs (_, _, t)) = occs_const t |
151 | occs_const (Abs (_, _, t)) = occs_const t |
152 | occs_const (t $ u) = occs_const t orelse occs_const u |
152 | occs_const (t $ u) = occs_const t orelse occs_const u |
153 | occs_const _ = false; |
153 | occs_const _ = false; |
154 |
154 |
155 val show_frees = commas_quote o map (fst o dest_Free); |
155 val show_frees = commas_quote o map (fst o dest_Free); |
166 else if not (null rhs_extras) then |
166 else if not (null rhs_extras) then |
167 err ("Extra variables on rhs: " ^ show_frees rhs_extras) |
167 err ("Extra variables on rhs: " ^ show_frees rhs_extras) |
168 else if not (null rhs_extrasT) then |
168 else if not (null rhs_extrasT) then |
169 err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) |
169 err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT) |
170 else if occs_const rhs then |
170 else if occs_const rhs then |
171 err ("Constant " ^ quote c ^ " occurs on rhs") |
171 err ("Constant to be defined occurs on rhs") |
172 else (c, ty) |
172 else (c, ty) |
173 end; |
173 end; |
174 |
174 |
175 |
175 |
176 (* check_defn *) |
176 (* check_defn *) |