17 |
17 |
18 local fun tybind (x,y) = (TVar (x,["term"]) , y) |
18 local fun tybind (x,y) = (TVar (x,["term"]) , y) |
19 fun tmbind (x,y) = (Var (x,type_of y), y) |
19 fun tmbind (x,y) = (Var (x,type_of y), y) |
20 in |
20 in |
21 fun match_term thry pat ob = |
21 fun match_term thry pat ob = |
22 let val tsig = #tsig(Sign.rep_sg(sign_of thry)) |
22 let val tsig = #tsig(Sign.rep_sg(Theory.sign_of thry)) |
23 val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) |
23 val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) |
24 in (map tmbind tm_theta, map tybind ty_theta) |
24 in (map tmbind tm_theta, map tybind ty_theta) |
25 end |
25 end |
26 |
26 |
27 fun match_type thry pat ob = |
27 fun match_type thry pat ob = |
28 map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob))) |
28 map tybind(Type.typ_match (#tsig(Sign.rep_sg(Theory.sign_of thry))) ([],(pat,ob))) |
29 end; |
29 end; |
30 |
30 |
31 |
31 |
32 (*--------------------------------------------------------------------------- |
32 (*--------------------------------------------------------------------------- |
33 * Typing |
33 * Typing |
34 *---------------------------------------------------------------------------*) |
34 *---------------------------------------------------------------------------*) |
35 |
35 |
36 fun typecheck thry = cterm_of (sign_of thry); |
36 fun typecheck thry = Thm.cterm_of (Theory.sign_of thry); |
37 |
37 |
38 |
38 |
39 (*--------------------------------------------------------------------------- |
39 (*--------------------------------------------------------------------------- |
40 * Get information about datatypes |
40 * Get information about datatypes |
41 *---------------------------------------------------------------------------*) |
41 *---------------------------------------------------------------------------*) |