--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 05 11:57:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Thu Mar 05 11:57:34 2015 +0100
@@ -8,6 +8,7 @@
signature BNF_FP_REC_SUGAR_UTIL =
sig
+ val error_at: Proof.context -> term list -> string -> 'a
datatype fp_kind = Least_FP | Greatest_FP
@@ -57,6 +58,10 @@
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL =
struct
+fun error_at ctxt ts str =
+ error (str ^ (if null ts then ""
+ else " at\n " ^ space_implode "\n " (map (quote o Syntax.string_of_term ctxt) ts)));
+
datatype fp_kind = Least_FP | Greatest_FP;
fun case_fp Least_FP l _ = l