# HG changeset patch
# User wenzelm
# Date 1364660001 -3600
# Node ID c52891242de2196b33c615bfce3f4d7722115b5a
# Parent  8ea0a5dd5a35b1d675b5d4970e52eb5001fa3d9a
more formal cong_name;

diff -r 8ea0a5dd5a35 -r c52891242de2 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat Mar 30 16:34:02 2013 +0100
+++ b/src/Pure/raw_simplifier.ML	Sat Mar 30 17:13:21 2013 +0100
@@ -15,6 +15,7 @@
   val simp_trace_depth_limit: int Config.T
   val simp_debug: bool Config.T
   val simp_trace: bool Config.T
+  type cong_name = bool * string
   type rrule
   val eq_rrule: rrule * rrule -> bool
   type simpset
@@ -26,8 +27,8 @@
   val dest_ss: simpset ->
    {simps: (string * thm) list,
     procs: (string * cterm list) list,
-    congs: (string * thm) list,
-    weak_congs: string list,
+    congs: (cong_name * thm) list,
+    weak_congs: cong_name list,
     loopers: string list,
     unsafe_solvers: string list,
     safe_solvers: string list}
@@ -72,7 +73,7 @@
     bounds: int * ((string * typ) * string) list,
     depth: int * bool Unsynchronized.ref,
     context: Proof.context option} *
-   {congs: (string * thm) list * string list,
+   {congs: (cong_name * thm) list * cong_name list,
     procs: proc Net.net,
     mk_rews:
      {mk: simpset -> thm -> thm list,
@@ -135,6 +136,15 @@
 
 (** datatype simpset **)
 
+(* congruence rules *)
+
+type cong_name = bool * string;
+
+fun cong_name (Const (a, _)) = SOME (true, a)
+  | cong_name (Free (a, _)) = SOME (false, a)
+  | cong_name _ = NONE;
+
+
 (* rewrite rules *)
 
 type rrule =
@@ -188,7 +198,7 @@
     bounds: int * ((string * typ) * string) list,
     depth: int * bool Unsynchronized.ref,
     context: Proof.context option} *
-   {congs: (string * thm) list * string list,
+   {congs: (cong_name * thm) list * cong_name list,
     procs: proc Net.net,
     mk_rews:
      {mk: simpset -> thm -> thm list,
@@ -268,7 +278,8 @@
 val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   (rules, prems, bounds,
     (depth + 1,
-      if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
+      if depth = simp_trace_depth_limit_of context
+      then Unsynchronized.ref false else exceeded), context));
 
 fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
 
@@ -538,10 +549,6 @@
 
 (* congs *)
 
-fun cong_name (Const (a, _)) = SOME a
-  | cong_name (Free (a, _)) = SOME ("Free: " ^ a)
-  | cong_name _ = NONE;
-
 local
 
 fun is_full_cong_prems [] [] = true
@@ -582,7 +589,7 @@
       val (xs, weak) = congs;
       val _ =
         if AList.defined (op =) xs a
-        then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
+        then if_visible ss warning ("Overwriting congruence rule for " ^ quote (#2 a))
         else ();
       val xs' = AList.update (op =) (a, thm) xs;
       val weak' = if is_full_cong thm then weak else a :: weak;
@@ -597,7 +604,7 @@
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", thm);
       val (xs, _) = congs;
-      val xs' = filter_out (fn (x : string, _) => x = a) xs;
+      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);
@@ -876,7 +883,7 @@
 
 fun uncond_skel ((_, weak), (lhs, rhs)) =
   if null weak then rhs  (*optimization*)
-  else if exists_Const (member (op =) weak o #1) lhs then skel0
+  else if exists_Const (fn (c, _) => member (op =) weak (true, c)) lhs then skel0
   else rhs;
 
 (*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
diff -r 8ea0a5dd5a35 -r c52891242de2 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Mar 30 16:34:02 2013 +0100
+++ b/src/Pure/simplifier.ML	Sat Mar 30 17:13:21 2013 +0100
@@ -119,14 +119,17 @@
 
 fun pretty_ss ctxt ss =
   let
-    val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
+    val pretty_term = Syntax.pretty_term ctxt;
     val pretty_thm = Display.pretty_thm ctxt;
     val pretty_thm_item = Display.pretty_thm_item ctxt;
 
     fun pretty_proc (name, lhss) =
-      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
+      Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_term o Thm.term_of) lhss);
+
+    fun pretty_cong_name (const, name) =
+      pretty_term ((if const then Const else Free) (name, dummyT));
     fun pretty_cong (name, thm) =
-      Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, pretty_thm thm];
+      Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm];
 
     val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
   in