--- a/src/HOL/Tools/function_package/context_tree.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML Tue Jun 06 08:21:14 2006 +0200
@@ -82,7 +82,6 @@
-exception CTREE_INTERNAL of string
fun find_cong_rule thy ((r,dep)::rs) t =
(let
@@ -95,7 +94,7 @@
(r, dep, branches)
end
handle Pattern.MATCH => find_cong_rule thy rs t)
- | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *)
+ | find_cong_rule thy [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
fun matchcall f (a $ b) = if a = f then SOME b else NONE