1.1 --- a/src/Pure/raw_simplifier.ML	Sat Mar 30 16:34:02 2013 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Sat Mar 30 17:13:21 2013 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4    val simp_trace_depth_limit: int Config.T
     1.5    val simp_debug: bool Config.T
     1.6    val simp_trace: bool Config.T
     1.7 +  type cong_name = bool * string
     1.8    type rrule
     1.9    val eq_rrule: rrule * rrule -> bool
    1.10    type simpset
    1.11 @@ -26,8 +27,8 @@
    1.12    val dest_ss: simpset ->
    1.13     {simps: (string * thm) list,
    1.14      procs: (string * cterm list) list,
    1.15 -    congs: (string * thm) list,
    1.16 -    weak_congs: string list,
    1.17 +    congs: (cong_name * thm) list,
    1.18 +    weak_congs: cong_name list,
    1.19      loopers: string list,
    1.20      unsafe_solvers: string list,
    1.21      safe_solvers: string list}
    1.22 @@ -72,7 +73,7 @@
    1.23      bounds: int * ((string * typ) * string) list,
    1.24      depth: int * bool Unsynchronized.ref,
    1.25      context: Proof.context option} *
    1.26 -   {congs: (string * thm) list * string list,
    1.27 +   {congs: (cong_name * thm) list * cong_name list,
    1.28      procs: proc Net.net,
    1.29      mk_rews:
    1.30       {mk: simpset -> thm -> thm list,
    1.31 @@ -135,6 +136,15 @@
    1.32  
    1.33  (** datatype simpset **)
    1.34  
    1.35 +(* congruence rules *)
    1.36 +
    1.37 +type cong_name = bool * string;
    1.38 +
    1.39 +fun cong_name (Const (a, _)) = SOME (true, a)
    1.40 +  | cong_name (Free (a, _)) = SOME (false, a)
    1.41 +  | cong_name _ = NONE;
    1.42 +
    1.43 +
    1.44  (* rewrite rules *)
    1.45  
    1.46  type rrule =
    1.47 @@ -188,7 +198,7 @@
    1.48      bounds: int * ((string * typ) * string) list,
    1.49      depth: int * bool Unsynchronized.ref,
    1.50      context: Proof.context option} *
    1.51 -   {congs: (string * thm) list * string list,
    1.52 +   {congs: (cong_name * thm) list * cong_name list,
    1.53      procs: proc Net.net,
    1.54      mk_rews:
    1.55       {mk: simpset -> thm -> thm list,
    1.56 @@ -268,7 +278,8 @@
    1.57  val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
    1.58    (rules, prems, bounds,
    1.59      (depth + 1,
    1.60 -      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
    1.61 +      if depth = simp_trace_depth_limit_of context
    1.62 +      then Unsynchronized.ref false else exceeded), context));
    1.63  
    1.64  fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
    1.65  
    1.66 @@ -538,10 +549,6 @@
    1.67  
    1.68  (* congs *)
    1.69  
    1.70 -fun cong_name (Const (a, _)) = SOME a
    1.71 -  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
    1.72 -  | cong_name _ = NONE;
    1.73 -
    1.74  local
    1.75  
    1.76  fun is_full_cong_prems [] [] = true
    1.77 @@ -582,7 +589,7 @@
    1.78        val (xs, weak) = congs;
    1.79        val _ =
    1.80          if AList.defined (op =) xs a
    1.81 -        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
    1.82 +        then if_visible ss warning ("Overwriting congruence rule for " ^ quote (#2 a))
    1.83          else ();
    1.84        val xs' = AList.update (op =) (a, thm) xs;
    1.85        val weak' = if is_full_cong thm then weak else a :: weak;
    1.86 @@ -597,7 +604,7 @@
    1.87        val a = the (cong_name (head_of lhs)) handle Option.Option =>
    1.88          raise SIMPLIFIER ("Congruence must start with a constant", thm);
    1.89        val (xs, _) = congs;
    1.90 -      val xs' = filter_out (fn (x : string, _) => x = a) xs;
    1.91 +      val xs' = filter_out (fn (x : cong_name, _) => x = a) xs;
    1.92        val weak' = xs' |> map_filter (fn (a, thm) =>
    1.93          if is_full_cong thm then NONE else SOME a);
    1.94      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
    1.95 @@ -876,7 +883,7 @@
    1.96  
    1.97  fun uncond_skel ((_, weak), (lhs, rhs)) =
    1.98    if null weak then rhs  (*optimization*)
    1.99 -  else if exists_Const (member (op =) weak o #1) lhs then skel0
   1.100 +  else if exists_Const (fn (c, _) => member (op =) weak (true, c)) lhs then skel0
   1.101    else rhs;
   1.102  
   1.103  (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.

     2.1 --- a/src/Pure/simplifier.ML	Sat Mar 30 16:34:02 2013 +0100
     2.2 +++ b/src/Pure/simplifier.ML	Sat Mar 30 17:13:21 2013 +0100
     2.3 @@ -119,14 +119,17 @@
     2.4  
     2.5  fun pretty_ss ctxt ss =
     2.6    let
     2.7 -    val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
     2.8 +    val pretty_term = Syntax.pretty_term ctxt;
     2.9      val pretty_thm = Display.pretty_thm ctxt;
    2.10      val pretty_thm_item = Display.pretty_thm_item ctxt;
    2.11  
    2.12      fun pretty_proc (name, lhss) =
    2.13 -      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
    2.14 +      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
    2.15 +
    2.16 +    fun pretty_cong_name (const, name) =
    2.17 +      pretty_term ((if const then Const else Free) (name, dummyT));
    2.18      fun pretty_cong (name, thm) =
    2.19 -      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
    2.20 +      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
    2.21  
    2.22      val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
    2.23    in