diff -r dce2168b0ea4 -r c62720b20e9a src/HOL/Tools/function_package/context_tree.ML
--- 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