avoid ML print in production code;
authorwenzelm
Sun, 11 Nov 2007 17:18:38 +0100
changeset 25402 0a1005435e11
parent 25401 5f818e7a46b5
child 25403 359b179fc963
avoid ML print in production code;
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], [])