1085 Unify.unifiers (@{theory}, init, [(trm1, trm2)]) |
1085 Unify.unifiers (@{theory}, init, [(trm1, trm2)]) |
1086 |> Seq.pull |
1086 |> Seq.pull |
1087 end" |
1087 end" |
1088 "NONE"} |
1088 "NONE"} |
1089 |
1089 |
1090 In order to find a |
1090 In order to find a reasonable solution for a unification problem, Isabelle |
1091 reasonable solution for a unification problem, Isabelle also tries first to |
1091 also tries first to solve the problem by higher-order pattern |
1092 solve the problem by higher-order pattern unification. |
1092 unification. Only in case of failure full higher-order unification is |
|
1093 called. This function has a built-in bound, which can be accessed and |
|
1094 manipulated as a configuration value: |
|
1095 |
|
1096 @{ML_response_fake [display,gray] |
|
1097 "Config.get_thy @{theory} (Unify.search_bound_value)" |
|
1098 "Int 60"} |
|
1099 |
|
1100 If this bound is reached during unification, Isabelle prints out the |
|
1101 warning message @{text [quotes] "Unification bound exceeded"} and |
|
1102 plenty of diagnostic information. |
|
1103 |
1093 |
1104 |
1094 For higher-order matching the function is called @{ML_ind matchers in Unify} |
1105 For higher-order matching the function is called @{ML_ind matchers in Unify} |
1095 implemented in the structure @{ML_struct Unify}. Also this function returns |
1106 implemented in the structure @{ML_struct Unify}. Also this function returns |
1096 sequences with possibly more than one matcher. Like @{ML unifiers in |
1107 sequences with possibly more than one matcher. Like @{ML unifiers in |
1097 Unify}, this function does not raise an exception in case of failure, but |
1108 Unify}, this function does not raise an exception in case of failure, but |