equal
deleted
inserted
replaced
10 TODO: optimize red by special-casing it |
10 TODO: optimize red by special-casing it |
11 *) |
11 *) |
12 |
12 |
13 signature PATTERN = |
13 signature PATTERN = |
14 sig |
14 sig |
15 val unify_trace_failure_default: bool Unsynchronized.ref |
|
16 val unify_trace_failure_raw: Config.raw |
15 val unify_trace_failure_raw: Config.raw |
17 val unify_trace_failure: bool Config.T |
16 val unify_trace_failure: bool Config.T |
18 val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
17 val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
19 val first_order_match: theory -> term * term |
18 val first_order_match: theory -> term * term |
20 -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
19 -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv |
38 struct |
37 struct |
39 |
38 |
40 exception Unif; |
39 exception Unif; |
41 exception Pattern; |
40 exception Pattern; |
42 |
41 |
43 val unify_trace_failure_default = Unsynchronized.ref false; |
|
44 val unify_trace_failure_raw = |
42 val unify_trace_failure_raw = |
45 Config.declare_global ("unify_trace_failure", @{here}) |
43 Config.declare_global ("unify_trace_failure", @{here}) (fn _ => Config.Bool false); |
46 (fn _ => Config.Bool (! unify_trace_failure_default)); |
|
47 val unify_trace_failure = Config.bool unify_trace_failure_raw; |
44 val unify_trace_failure = Config.bool unify_trace_failure_raw; |
48 |
45 |
49 fun string_of_term thy env binders t = |
46 fun string_of_term thy env binders t = |
50 Syntax.string_of_term_global thy |
47 Syntax.string_of_term_global thy |
51 (Envir.norm_term env (subst_bounds (map Free binders, t))); |
48 (Envir.norm_term env (subst_bounds (map Free binders, t))); |