tuned signature;
authorwenzelm
Sun Jan 12 13:16:00 2014 +0100 (2014-01-12)
changeset 54997811c35e81ac5
parent 54996 aee15e11ee73
child 54998 8601434fa334
tuned signature;
src/Pure/raw_simplifier.ML
     1.1 --- a/src/Pure/raw_simplifier.ML	Sat Jan 11 23:53:38 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sun Jan 12 13:16:00 2014 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4  signature RAW_SIMPLIFIER =
     1.5  sig
     1.6    include BASIC_RAW_SIMPLIFIER
     1.7 -  exception SIMPLIFIER of string * thm
     1.8 +  exception SIMPLIFIER of string * thm list
     1.9    type trace_ops
    1.10    val set_trace_ops: trace_ops -> theory -> theory
    1.11    val internal_ss: simpset ->
    1.12 @@ -436,7 +436,7 @@
    1.13  
    1.14  (* diagnostics *)
    1.15  
    1.16 -exception SIMPLIFIER of string * thm;
    1.17 +exception SIMPLIFIER of string * thm list;
    1.18  
    1.19  val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
    1.20  val simp_debug = Config.bool simp_debug_raw;
    1.21 @@ -541,7 +541,7 @@
    1.22      val prems = Logic.strip_imp_prems prop;
    1.23      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
    1.24      val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
    1.25 -      raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
    1.26 +      raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
    1.27      val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
    1.28      val erhs = Envir.eta_contract (term_of rhs);
    1.29      val perm =
    1.30 @@ -554,7 +554,7 @@
    1.31  
    1.32  fun decomp_simp' thm =
    1.33    let val (_, lhs, _, rhs, _) = decomp_simp thm in
    1.34 -    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
    1.35 +    if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", [thm])
    1.36      else (lhs, rhs)
    1.37    end;
    1.38  
    1.39 @@ -666,10 +666,10 @@
    1.40    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.41      let
    1.42        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
    1.43 -        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.44 +        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
    1.45      (*val lhs = Envir.eta_contract lhs;*)
    1.46        val a = the (cong_name (head_of lhs)) handle Option.Option =>
    1.47 -        raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
    1.48 +        raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
    1.49        val (xs, weak) = congs;
    1.50        val _ =
    1.51          if AList.defined (op =) xs a then
    1.52 @@ -684,10 +684,10 @@
    1.53    (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.54      let
    1.55        val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
    1.56 -        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
    1.57 +        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", [thm]);
    1.58      (*val lhs = Envir.eta_contract lhs;*)
    1.59        val a = the (cong_name (head_of lhs)) handle Option.Option =>
    1.60 -        raise SIMPLIFIER ("Congruence must start with a constant", thm);
    1.61 +        raise SIMPLIFIER ("Congruence must start with a constant", [thm]);
    1.62        val (xs, _) = congs;
    1.63        val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
    1.64        val weak' = xs' |> map_filter (fn (a, thm) =>