equal
deleted
inserted
replaced
1097 "Config.get_thy @{theory} (Unify.search_bound_value)" |
1097 "Config.get_thy @{theory} (Unify.search_bound_value)" |
1098 "Int 60"} |
1098 "Int 60"} |
1099 |
1099 |
1100 If this bound is reached during unification, Isabelle prints out the |
1100 If this bound is reached during unification, Isabelle prints out the |
1101 warning message @{text [quotes] "Unification bound exceeded"} and |
1101 warning message @{text [quotes] "Unification bound exceeded"} and |
1102 plenty of diagnostic information. |
1102 plenty of diagnostic information (sometimes annoyingly plenty of |
|
1103 information). |
1103 |
1104 |
1104 |
1105 |
1105 For higher-order matching the function is called @{ML_ind matchers in Unify} |
1106 For higher-order matching the function is called @{ML_ind matchers in Unify} |
1106 implemented in the structure @{ML_struct Unify}. Also this function returns |
1107 implemented in the structure @{ML_struct Unify}. Also this function returns |
1107 sequences with possibly more than one matcher. Like @{ML unifiers in |
1108 sequences with possibly more than one matcher. Like @{ML unifiers in |