equal
deleted
inserted
replaced
312 Const (name, _) => name mem_string constr_consts |
312 Const (name, _) => name mem_string constr_consts |
313 | _ => false) end)) |
313 | _ => false) end)) |
314 else false |
314 else false |
315 *) |
315 *) |
316 |
316 |
317 (* must be exported in code.ML *) |
317 val is_constr = Code.is_constr; |
318 (* TODO: is there copy in the core? *) |
|
319 fun is_constr thy = is_some o Code.get_datatype_of_constr thy; |
|
320 |
318 |
321 fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = |
319 fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) = |
322 let |
320 let |
323 val (xTs, t') = strip_ex t |
321 val (xTs, t') = strip_ex t |
324 in |
322 in |