diff -r 5c211dd7e5ad -r ab9e09076462 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sat May 09 18:50:01 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Sun May 17 16:22:27 2009 +0200
@@ -212,7 +212,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = writeln (str_of_thm_no_vars ctxt thm)
+  val _ = writeln (string_of_thm_no_vars ctxt thm)
 in 
   Seq.single thm
 end*}
@@ -538,17 +538,17 @@
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} = 
 let 
-  val str_of_params = str_of_cterms context params
-  val str_of_asms = str_of_cterms context asms
-  val str_of_concl = str_of_cterm context concl
-  val str_of_prems = str_of_thms_no_vars context prems   
-  val str_of_schms = str_of_cterms context (snd schematics)    
+  val string_of_params = string_of_cterms context params
+  val string_of_asms = string_of_cterms context asms
+  val string_of_concl = string_of_cterm context concl
+  val string_of_prems = string_of_thms_no_vars context prems   
+  val string_of_schms = string_of_cterms context (snd schematics)    
  
-  val _ = (writeln ("params: " ^ str_of_params);
-           writeln ("schematics: " ^ str_of_schms);
-           writeln ("assumptions: " ^ str_of_asms);
-           writeln ("conclusion: " ^ str_of_concl);
-           writeln ("premises: " ^ str_of_prems))
+  val _ = (writeln ("params: " ^ string_of_params);
+           writeln ("schematics: " ^ string_of_schms);
+           writeln ("assumptions: " ^ string_of_asms);
+           writeln ("conclusion: " ^ string_of_concl);
+           writeln ("premises: " ^ string_of_prems))
 in
   no_tac 
 end*}
@@ -1182,9 +1182,9 @@
   val {simps, congs, procs, ...} = Simplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
-      "  " ^ nm ^ ": " ^ (str_of_thm_no_vars ctxt thm)
+      "  " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm)
   fun name_ctrm (nm, ctrm) =
-      "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
+      "  " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm)
 
   val s = ["Simplification rules:"] @ map name_thm simps @
           ["Congruences rules:"] @ map name_thm congs @
@@ -1497,6 +1497,8 @@
 
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
+  (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+
 *}
 
 section {* Simprocs *}
@@ -1516,7 +1518,7 @@
 ML %linenosgray{*fun fail_simproc simpset redex = 
 let
   val ctxt = Simplifier.the_context simpset
-  val _ = writeln ("The redex: " ^ (str_of_cterm ctxt redex))
+  val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex))
 in
   NONE
 end*}