equal
deleted
inserted
replaced
32 |
32 |
33 in |
33 in |
34 |
34 |
35 fun match_term thry pat ob = |
35 fun match_term thry pat ob = |
36 let |
36 let |
37 val tsig = Sign.tsig_of (Theory.sign_of thry) |
37 val (ty_theta, tm_theta) = Pattern.match thry (pat,ob) |
38 val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob) |
|
39 fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) |
38 fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) |
40 in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) |
39 in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) |
41 end; |
40 end; |
42 |
41 |
43 fun match_type thry pat ob = |
42 fun match_type thry pat ob = |
49 (*--------------------------------------------------------------------------- |
48 (*--------------------------------------------------------------------------- |
50 * Typing |
49 * Typing |
51 *---------------------------------------------------------------------------*) |
50 *---------------------------------------------------------------------------*) |
52 |
51 |
53 fun typecheck thry t = |
52 fun typecheck thry t = |
54 Thm.cterm_of (Theory.sign_of thry) t |
53 Thm.cterm_of thry t |
55 handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
54 handle TYPE (msg, _, _) => raise THRY_ERR "typecheck" msg |
56 | TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
55 | TERM (msg, _) => raise THRY_ERR "typecheck" msg; |
57 |
56 |
58 |
57 |
59 (*--------------------------------------------------------------------------- |
58 (*--------------------------------------------------------------------------- |