--- a/CookBook/Tactical.thy	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Tactical.thy	Sun Mar 08 20:53:00 2009 +0000
@@ -1119,58 +1119,44 @@
 text_raw {*
 \begin{figure}[tp]
 \begin{isabelle}*}
-ML{*fun get_parts ss = 
-let 
-  val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss
-  
-  val rules_list = Net.entries rules
-  val rnames = map #name rules_list
-  val rthms =  map #thm rules_list
-
-  val congs_list = fst congs
-  val cnames = map fst congs_list  
-  val cthms = map (#thm o snd) congs_list
-
-  val proc_list = Net.entries procs
-in
-  (rnames ~~ rthms, cnames ~~ cthms)
-end
-
-fun print_parts ctxt ss =
+ML{*fun print_ss ctxt ss =
 let
-  val (simps, congs) = get_parts ss
+  val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
       "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+  fun name_ctrm (nm, ctrm) =
+      "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 
   val s1 = ["Simplification rules:"]
   val s2 = map name_thm simps
   val s3 = ["Congruences rules:"]
   val s4 = map name_thm congs
+  val s5 = ["Simproc patterns:"]
+  val s6 = map name_ctrm procs
 in
-  (s1 @ s2 @ s3 @ s4) 
+  (s1 @ s2 @ s3 @ s4 @ s5 @ s6) 
      |> separate "\n"
      |> implode
      |> warning
 end*}
 text_raw {* 
 \end{isabelle}
-\caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing
-  a simpset. We are here only interested in the simplifcation rules, congruence rules and
-  simprocs. The first and third are discrimination nets, which from which we extract
-  lists using @{ML Net.entries}. The congruence rules are stored in 
-  an association list, associating a constant with a rule.\label{fig:prettyss}}
+\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
+  all printable information stored in a simpset. We are here only interested in the 
+  simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 
 text {* 
-  To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which
+  To see how they work, consider the two functions in Figure~\ref{fig:printss}, which
   print out some parts of a simpset. If you use them to print out the components of the
   empty simpset, in ML @{ML empty_ss} and the most primitive simpset
   
   @{ML_response_fake [display,gray]
-  "print_parts @{context} empty_ss"
+  "print_ss @{context} empty_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   you can see it contains nothing. This simpset is usually not useful, except as a 
   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
@@ -1183,10 +1169,11 @@
   Printing then out the components of the simpset gives:
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} ss1"
+  "print_ss @{context} ss1"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   (FIXME: Why does it print out ??.unknown)
 
@@ -1199,11 +1186,12 @@
   gives
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} ss2"
+  "print_ss @{context} ss2"
 "Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"}
+  UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
+Simproc patterns:"}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
   expects this form of the simplification and congruence rules. However, even 
@@ -1213,9 +1201,10 @@
   printing out the components of this simpset
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} HOL_basic_ss"
+  "print_ss @{context} HOL_basic_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 
   also produces ``nothing'', the printout is misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1239,7 +1228,7 @@
   connectives in HOL. 
 
   @{ML_response_fake [display,gray]
-  "print_parts @{context} HOL_ss"
+  "print_ss @{context} HOL_ss"
 "Simplification rules:
   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
   HOL.the_eq_trivial: THE x. x = y \<equiv> y
@@ -1248,7 +1237,9 @@
 Congruences rules:
   HOL.simp_implies: \<dots>
     \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
-  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"}
+  op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+Simproc patterns:
+  \<dots>"}
 
   
   The simplifier is often used to unfold definitions in a proof. For this the
@@ -1418,9 +1409,6 @@
 
   (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
 
-  (FIXME: Unfortunately one cannot access any simproc, as there is 
-  no @{text rep_proc} in function @{ML get_parts}.)
-
   (FIXME: What are the second components of the congruence rules---something to
   do with weak congruence constants?)