--- a/ProgTutorial/FirstSteps.thy	Tue Jul 14 16:34:24 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Jul 20 16:52:59 2009 +0200
@@ -1305,8 +1305,35 @@
 
   (FIXME: how to add case-names to goal states - maybe in the 
   next section)
+
+  (FIXME: example for how to add theorem styles)
 *}
 
+ML {*
+fun strip_assums_all (params, Const("all",_) $ Abs(a, T, t)) =
+      strip_assums_all ((a, T)::params, t)
+  | strip_assums_all (params, B) = (params, B)
+
+fun style_parm_premise i ctxt t =
+  let val prems = Logic.strip_imp_prems t in
+    if i <= length prems
+    then let val (params,t) = strip_assums_all([], nth prems (i - 1))
+         in subst_bounds(map Free params, t) end
+    else error ("Not enough premises for prem" ^ string_of_int i ^
+      " in propositon: " ^ Syntax.string_of_term ctxt t)
+  end;
+*}
+
+ML {*
+strip_assums_all ([], @{term "\<And>x y. A x y"})
+*}
+
+setup {*
+  TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
+  TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
+*}
+
+
 section {* Setups (TBD) *}
 
 text {*
@@ -1675,11 +1702,11 @@
   properly treats ``data slots''!
 
   Since storing theorems in a list is such a common task, there is the special
-  functor @{text NamedThmsFun}, which does most of the work for you. To obtain
+  functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
   a named theorem lists, you just declare
 *}
 
-ML{*structure FooRules = NamedThmsFun 
+ML{*structure FooRules = Named_Thms
  (val name = "foo" 
   val description = "Rules for foo") *}