equal
deleted
inserted
replaced
38 fun plural sg pl [x] = sg |
38 fun plural sg pl [x] = sg |
39 | plural sg pl _ = pl |
39 | plural sg pl _ = pl |
40 |
40 |
41 |
41 |
42 (* Removes all quantifiers from a term, replacing bound variables by frees. *) |
42 (* Removes all quantifiers from a term, replacing bound variables by frees. *) |
43 fun dest_all_all (t as (Const ("all",_) $ _)) = |
43 fun dest_all_all (t as (Const (@{const_name Pure.all},_) $ _)) = |
44 let |
44 let |
45 val (v,b) = Logic.dest_all t |> apfst Free |
45 val (v,b) = Logic.dest_all t |> apfst Free |
46 val (vs, b') = dest_all_all b |
46 val (vs, b') = dest_all_all b |
47 in |
47 in |
48 (v :: vs, b') |
48 (v :: vs, b') |