src/Pure/raw_simplifier.ML

 end;
 
 signature RAW_SIMPLIFIER =
 sig
   include BASIC_RAW_SIMPLIFIER
-  exception SIMPLIFIER of string * thm
+  exception SIMPLIFIER of string * thm list
   type trace_ops
   val set_trace_ops: trace_ops -> theory -> theory
   val internal_ss: simpset ->
    {congs: (cong_name * thm) list * cong_name list,
     procs: proc Net.net,

   in depth end;
 
 
 (* diagnostics *)
 
-exception SIMPLIFIER of string * thm;
+exception SIMPLIFIER of string * thm list;
 
 val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
 val simp_debug = Config.bool simp_debug_raw;
 
 val simp_trace_default = Unsynchronized.ref false;

   let
     val prop = Thm.prop_of thm;
     val prems = Logic.strip_imp_prems prop;
     val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
     val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
-      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
+      raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
     val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
     val erhs = Envir.eta_contract (term_of rhs);
     val perm =
       var_perm (term_of elhs, erhs) andalso
       not (term_of elhs aconv erhs) andalso

 
 end;
 
 fun decomp_simp' thm =
   let val (_, lhs, _, rhs, _) = decomp_simp thm in
-    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
+    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm])
     else (lhs, rhs)
   end;
 
 fun mk_eq_True ctxt (thm, name) =
   let val Simpset (_, {mk_rews = {mk_eq_True, ...}, ...}) = simpset_of ctxt in

 
 fun add_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
-        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
-        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
+        raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
       val (xs, weak) = congs;
       val _ =
         if AList.defined (op =) xs a then
           Context_Position.if_visible ctxt
             warning ("Overwriting congruence rule for " ^ quote (#2 a))

 
 fun del_eqcong thm ctxt = ctxt |> map_simpset2
   (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
-        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
-        raise SIMPLIFIER ("Congruence must start with a constant", thm);
+        raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
       val (xs, _) = congs;
       val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
       val weak' = xs' |> map_filter (fn (a, thm) =>
         if is_full_cong thm then NONE else SOME a);
     in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);