# HG changeset patch
# User wenzelm
# Date 1194797918 -3600
# Node ID 0a1005435e110e72bd1cf115ebcdcffa8e91b123
# Parent  5f818e7a46b5061e978499189a5bdcc00efddd4a
avoid ML print in production code;

diff -r 5f818e7a46b5 -r 0a1005435e11 src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Sun Nov 11 16:58:41 2007 +0100
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Sun Nov 11 17:18:38 2007 +0100
@@ -42,7 +42,7 @@
 fun inst_constrs_of thy (T as Type (name, _)) =
     map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
         (the (DatatypePackage.get_datatype_constrs thy name))
-  | inst_constrs_of thy t = (print t; sys_error "inst_constrs_of")
+  | inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], [])