tuned;

--- a/NEWS	Fri Nov 25 17:41:52 2005 +0100
+++ b/NEWS	Fri Nov 25 18:58:34 2005 +0100
@@ -78,10 +78,10 @@
     shows "P n x"
     using a                     -- {* make induct insert fact a *}
   proof (induct n fixing: x)    -- {* generalize goal to "!!x. A n x ==> P n x" *}
-    case (0 x)
+    case 0
     show ?case sorry
   next
-    case (Suc n x)
+    case (Suc n)
     note `!!x. A n x ==> P n x` -- {* induction hypothesis, according to induction rule *}
     note `A (Suc n) x`          -- {* induction premise, stemming from fact a *}
     show ?case sorry

--- a/src/Pure/logic.ML	Fri Nov 25 17:41:52 2005 +0100
+++ b/src/Pure/logic.ML	Fri Nov 25 18:58:34 2005 +0100
@@ -229,21 +229,21 @@
 end;
 
 
-(*Make lifting functions from subgoal and increment.
+(* Lifting functions from subgoal and increment:
     lift_abs operates on terms
     lift_all operates on propositions *)
 
 fun lift_abs inc =
   let
     fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t
-      | lift Ts (Const ("all", _) $ Abs (a, T, b)) t = Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t)
       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   in lift [] end;
 
 fun lift_all inc =
   let
     fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t
-      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, b)) t = c $ Abs (a, T, lift (T :: Ts) b t)
+      | lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t)
       | lift Ts _ t = incr_indexes (rev Ts, inc) t;
   in lift [] end;