diff --git a/src/HOL/Hoare/Hoare_Logic.thy b/src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy
+++ b/src/HOL/Hoare/Hoare_Logic.thy
@@ -1,217 +1,217 @@
 (*  Title:      HOL/Hoare/Hoare_Logic.thy
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Copyright   1998 TUM
     Author:     Walter Guttmann (extension to total-correctness proofs)
 *)
 
 section \<open>Hoare logic\<close>
 
 theory Hoare_Logic
   imports Hoare_Syntax Hoare_Tac
 begin
 
 subsection \<open>Sugared semantic embedding of Hoare logic\<close>
 
 text \<open>
   Strictly speaking a shallow embedding (as implemented by Norbert Galm
   following Mike Gordon) would suffice. Maybe the datatype com comes in useful
   later.
 \<close>
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
 
 datatype 'a com =
   Basic "'a \<Rightarrow> 'a"
 | Seq "'a com" "'a com"
 | Cond "'a bexp" "'a com" "'a com"
 | While "'a bexp" "'a com"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a => 'a => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
   "Sem (Basic f) s (f s)"
 | "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (Seq c1 c2) s s'"
 | "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
 | "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (Cond b c1 c2) s s'"
 | "s \<notin> b \<Longrightarrow> Sem (While b c) s s"
 | "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b c) s'' s' \<Longrightarrow>
    Sem (While b c) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "Valid p c a q \<equiv> \<forall>s s'. Sem c s s' \<longrightarrow> s \<in> p \<longrightarrow> s' \<in> q"
 
 definition ValidTC :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a anno \<Rightarrow> 'a bexp \<Rightarrow> bool"
   where "ValidTC p c a q \<equiv> \<forall>s. s \<in> p \<longrightarrow> (\<exists>t. Sem c s t \<and> t \<in> q)"
 
 inductive_cases [elim!]:
   "Sem (Basic f) s s'" "Sem (Seq c1 c2) s s'"
   "Sem (Cond b c1 c2) s s'"
 
 lemma Sem_deterministic:
   assumes "Sem c s s1"
       and "Sem c s s2"
     shows "s1 = s2"
 proof -
   have "Sem c s s1 \<Longrightarrow> (\<forall>s2. Sem c s s2 \<longrightarrow> s1 = s2)"
     by (induct rule: Sem.induct) (subst Sem.simps, blast)+
   thus ?thesis
     using assms by simp
 qed
 
 lemma tc_implies_pc:
   "ValidTC p c a q \<Longrightarrow> Valid p c a q"
   by (metis Sem_deterministic Valid_def ValidTC_def)
 
 lemma tc_extract_function:
   "ValidTC p c a q \<Longrightarrow> \<exists>f . \<forall>s . s \<in> p \<longrightarrow> f s \<in> q"
   by (metis ValidTC_def)
 
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) a q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) a q"
 by (auto simp:Valid_def)
 
 lemma SeqRule: "Valid P c1 a1 Q \<Longrightarrow> Valid Q c2 a2 R \<Longrightarrow> Valid P (Seq c1 c2) (Aseq a1 a2) R"
 by (auto simp:Valid_def)
 
 lemma CondRule:
  "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
   \<Longrightarrow> Valid w c1 a1 q \<Longrightarrow> Valid w' c2 a2 q \<Longrightarrow> Valid p (Cond b c1 c2) (Acond a1 a2) q"
 by (auto simp:Valid_def)
 
 lemma While_aux:
   assumes "Sem (While b c) s s'"
   shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
     s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
   using assms
   by (induct "While b c" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c (A 0) i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b c) (Awhile i v A) q"
 apply (clarsimp simp:Valid_def)
 apply(drule While_aux)
   apply assumption
  apply blast
 apply blast
 done
 
 lemma SkipRuleTC:
   assumes "p \<subseteq> q"
     shows "ValidTC p (Basic id) a q"
   by (metis assms Sem.intros(1) ValidTC_def id_apply subsetD)
 
 lemma BasicRuleTC:
   assumes "p \<subseteq> {s. f s \<in> q}"
     shows "ValidTC p (Basic f) a q"
   by (metis assms Ball_Collect Sem.intros(1) ValidTC_def)
 
 lemma SeqRuleTC:
   assumes "ValidTC p c1 a1 q"
       and "ValidTC q c2 a2 r"
     shows "ValidTC p (Seq c1 c2) (Aseq a1 a2) r"
   by (meson assms Sem.intros(2) ValidTC_def)
 
 lemma CondRuleTC:
  assumes "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}"
      and "ValidTC w c1 a1 q"
      and "ValidTC w' c2 a2 q"
    shows "ValidTC p (Cond b c1 c2) (Acond a1 a2) q"
 proof (unfold ValidTC_def, rule allI)
   fix s
   show "s \<in> p \<longrightarrow> (\<exists>t . Sem (Cond b c1 c2) s t \<and> t \<in> q)"
     apply (cases "s \<in> b")
     apply (metis (mono_tags, lifting) assms(1,2) Ball_Collect Sem.intros(3) ValidTC_def)
     by (metis (mono_tags, lifting) assms(1,3) Ball_Collect Sem.intros(4) ValidTC_def)
 qed
 
 lemma WhileRuleTC:
   assumes "p \<subseteq> i"
       and "\<And>n::nat . ValidTC (i \<inter> b \<inter> {s . v s = n}) c (A n) (i \<inter> {s . v s < n})"
       and "i \<inter> uminus b \<subseteq> q"
-    shows "ValidTC p (While b c) (Awhile i v A) q"
-proof -
+    shows "ValidTC p (While b c) (Awhile i v (\<lambda>n. A n)) q"
+proof -                             
   {
     fix s n
     have "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
     proof (induction "n" arbitrary: s rule: less_induct)
       fix n :: nat
       fix s :: 'a
       assume 1: "\<And>(m::nat) s::'a . m < n \<Longrightarrow> s \<in> i \<and> v s = m \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
       show "s \<in> i \<and> v s = n \<longrightarrow> (\<exists>t . Sem (While b c) s t \<and> t \<in> q)"
       proof (rule impI, cases "s \<in> b")
         assume 2: "s \<in> b" and "s \<in> i \<and> v s = n"
         hence "s \<in> i \<inter> b \<inter> {s . v s = n}"
           using assms(1) by auto
         hence "\<exists>t . Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by (metis assms(2) ValidTC_def)
         from this obtain t where 3: "Sem c s t \<and> t \<in> i \<inter> {s . v s < n}"
           by auto
         hence "\<exists>u . Sem (While b c) t u \<and> u \<in> q"
           using 1 by auto
         thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
           using 2 3 Sem.intros(6) by force
       next
         assume "s \<notin> b" and "s \<in> i \<and> v s = n"
         thus "\<exists>t . Sem (While b c) s t \<and> t \<in> q"
           using Sem.intros(5) assms(3) by fastforce
       qed
     qed
   }
   thus ?thesis
     using assms(1) ValidTC_def by force
 qed
 
 
 subsubsection \<open>Concrete syntax\<close>
 
 setup \<open>
   Hoare_Syntax.setup
    {Basic = \<^const_syntax>\<open>Basic\<close>,
     Skip = \<^const_syntax>\<open>annskip\<close>,
     Seq = \<^const_syntax>\<open>Seq\<close>,
     Cond = \<^const_syntax>\<open>Cond\<close>,
     While = \<^const_syntax>\<open>While\<close>,
     Valid = \<^const_syntax>\<open>Valid\<close>,
     ValidTC = \<^const_syntax>\<open>ValidTC\<close>}
 \<close>
 
 
 subsubsection \<open>Proof methods: VCG\<close>
 
 declare BasicRule [Hoare_Tac.BasicRule]
   and SkipRule [Hoare_Tac.SkipRule]
   and SeqRule [Hoare_Tac.SeqRule]
   and CondRule [Hoare_Tac.CondRule]
   and WhileRule [Hoare_Tac.WhileRule]
 
 declare BasicRuleTC [Hoare_Tac.BasicRuleTC]
   and SkipRuleTC [Hoare_Tac.SkipRuleTC]
   and SeqRuleTC [Hoare_Tac.SeqRuleTC]
   and CondRuleTC [Hoare_Tac.CondRuleTC]
   and WhileRuleTC [Hoare_Tac.WhileRuleTC]
 
 method_setup vcg = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 method_setup vcg_tc = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (K all_tac)))\<close>
   "verification condition generator"
 
 method_setup vcg_tc_simp = \<open>
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (Hoare_Tac.hoare_tc_tac ctxt (asm_full_simp_tac ctxt)))\<close>
   "verification condition generator plus simplification"
 
 end
diff --git a/src/HOL/Hoare/hoare_syntax.ML b/src/HOL/Hoare/hoare_syntax.ML
--- a/src/HOL/Hoare/hoare_syntax.ML
+++ b/src/HOL/Hoare/hoare_syntax.ML
@@ -1,252 +1,252 @@
 (*  Title:      HOL/Hoare/hoare_syntax.ML
     Author:     Leonor Prensa Nieto & Tobias Nipkow
     Author:     Walter Guttmann (initial extension to total-correctness proofs)
     Author:     Tobias Nipkow (complete version of total correctness with separate anno type)
 
 Syntax translations for Hoare logic.
 *)
 
 signature HOARE_SYNTAX =
 sig
   val hoare_vars_tr: Proof.context -> term list -> term
   val hoare_tc_vars_tr: Proof.context -> term list -> term
   val spec_tr': string -> Proof.context -> term list -> term
   val setup:
     {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
       Valid: string, ValidTC: string} -> theory -> theory
 end;
 
 structure Hoare_Syntax: HOARE_SYNTAX =
 struct
 
 (** theory data **)
 
 structure Data = Theory_Data
 (
   type T =
     {Basic: string, Skip: string, Seq: string, Cond: string, While: string,
       Valid: string, ValidTC: string} option;
   val empty: T = NONE;
   fun merge (data1, data2) =
     if is_some data1 andalso is_some data2 andalso data1 <> data2 then
       error "Cannot merge syntax from different Hoare Logics"
     else merge_options (data1, data2);
 );
 
 fun const_syntax ctxt which =
   (case Data.get (Proof_Context.theory_of ctxt) of
     SOME consts => which consts
   | NONE => error "Undefined Hoare syntax consts");
 
 val syntax_const = Syntax.const oo const_syntax;
 
 
 
 (** parse translation **)
 
 local
 
 fun idt_name (Free (x, _)) = SOME x
   | idt_name (Const (\<^syntax_const>\<open>_constrain\<close>, _) $ t $ _) = idt_name t
   | idt_name _ = NONE;
 
 fun eq_idt tu =
   (case apply2 idt_name tu of
     (SOME x, SOME y) => x = y
   | _ => false);
 
 fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body]
   | mk_abstuple (x :: xs) body =
       Syntax.const \<^const_syntax>\<open>case_prod\<close> $ Syntax_Trans.abs_tr [x, mk_abstuple xs body];
 
 fun mk_fbody x e [y] = if eq_idt (x, y) then e else y
   | mk_fbody x e (y :: xs) =
       Syntax.const \<^const_syntax>\<open>Pair\<close> $
         (if eq_idt (x, y) then e else y) $ mk_fbody x e xs;
 
 fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs);
 
 
 (* bexp_tr & assn_tr *)
 (*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
 
 fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE"   (* FIXME !? *)
   | bexp_tr b xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs b;
 
 fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r;
 
 fun var_tr v xs = mk_abstuple xs v;
 
 
 (* com_tr *)
 
 fun com_tr ctxt =
   let
     fun tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs =
           (syntax_const ctxt #Basic $ mk_fexp x e xs, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
       | tr (Const (\<^syntax_const>\<open>_Seq\<close>,_) $ c1 $ c2) xs =
           let val (c1',a1) = tr c1 xs;
               val (c2',a2) = tr c2 xs
           in (syntax_const ctxt #Seq $ c1' $ c2', Syntax.const \<^const_syntax>\<open>Aseq\<close> $ a1 $ a2) end
       | tr (Const (\<^syntax_const>\<open>_Cond\<close>,_) $ b $ c1 $ c2) xs =
           let val (c1',a1) = tr c1 xs;
               val (c2',a2) = tr c2 xs
           in (syntax_const ctxt #Cond $ bexp_tr b xs $ c1' $ c2',
               Syntax.const \<^const_syntax>\<open>Acond\<close> $ a1 $ a2)
           end
       | tr (Const (\<^syntax_const>\<open>_While\<close>,_) $ b $ i $ v $ c) xs =
           let val (c',a) = tr c xs
               val (v',A) = case v of
                 Const (\<^const_syntax>\<open>HOL.eq\<close>, _) $ z $ t => (t, Syntax_Trans.abs_tr [z, a]) |
-                t => (t, absdummy dummyT a)
+                t => (t, Abs ("n", dummyT, a))
           in (syntax_const ctxt #While $ bexp_tr b xs $ c',
               Syntax.const \<^const_syntax>\<open>Awhile\<close>
                 $ assn_tr i xs $ var_tr v' xs $ A)
           end
       | tr (Const (\<^syntax_const>\<open>_While0\<close>,_) $ b $ I $ c) xs =
           let val (c',a) = tr c xs
           in (syntax_const ctxt #While $ bexp_tr b xs $ c',
               Syntax.const \<^const_syntax>\<open>Awhile\<close>
                 $ assn_tr I xs $ var_tr (Syntax.const \<^const_syntax>\<open>zero_class.zero\<close>) xs
                 $ absdummy dummyT a)
           end
       | tr t _ = (t, Syntax.const \<^const_syntax>\<open>Abasic\<close>)
   in tr end;
 
 fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars
   | vars_tr t = [t];
 
 in
 
 fun hoare_vars_tr ctxt [vars, pre, prg, post] =
       let val xs = vars_tr vars
           val (c',a) = com_tr ctxt prg xs
       in syntax_const ctxt #Valid $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
   | hoare_vars_tr _ ts = raise TERM ("hoare_vars_tr", ts);
 
 fun hoare_tc_vars_tr ctxt [vars, pre, prg, post] =
       let val xs = vars_tr vars
           val (c',a) = com_tr ctxt prg xs
       in syntax_const ctxt #ValidTC $ assn_tr pre xs $ c' $ a $ assn_tr post xs end
   | hoare_tc_vars_tr _ ts = raise TERM ("hoare_tc_vars_tr", ts);
 
 end;
 
 
 
 (** print translation **)
 
 local
 
 fun dest_abstuple
       (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (v, _, body)) =
         subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple tm = tm;
 
 fun abs2list (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, _)) = [Free (x, T)]
   | abs2list _ = [];
 
 fun mk_ts (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (_, _, t)) = mk_ts t
   | mk_ts (Abs (_, _, t)) = mk_ts t
   | mk_ts (Const (\<^const_syntax>\<open>Pair\<close>, _) $ a $ b) = a :: mk_ts b
   | mk_ts t = [t];
 
 fun mk_vts (Const (\<^const_syntax>\<open>case_prod\<close>,_) $ Abs (x, _, t)) =
       (Syntax.free x :: abs2list t, mk_ts t)
   | mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t])
   | mk_vts _ = raise Match;
 
 fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch"))  (* FIXME no_ch!? *)
   | find_ch ((v, t) :: vts) i xs =
       if t = Bound i then find_ch vts (i - 1) xs
       else (true, (v, subst_bounds (xs, t)));
 
 fun is_f (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs _) = true
   | is_f (Abs _) = true
   | is_f _ = false;
 
 
 (* assn_tr' & bexp_tr'*)
 
 fun assn_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
   | assn_tr' (Const (\<^const_syntax>\<open>inter\<close>, _) $
         (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T1) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T2)) =
       Syntax.const \<^const_syntax>\<open>inter\<close> $ dest_abstuple T1 $ dest_abstuple T2
   | assn_tr' t = t;
 
 fun bexp_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T
   | bexp_tr' t = t;
 
 fun var_tr' xo T =
   let val n = dest_abstuple T
   in case xo of NONE => n | SOME x => Syntax.const \<^const_syntax>\<open>HOL.eq\<close> $ Syntax.free x $ n end
 
 
 (* com_tr' *)
 
 fun mk_assign ctxt f =
   let
     val (vs, ts) = mk_vts f;
     val (ch, (a, b)) = find_ch (vs ~~ ts) (length vs - 1) (rev vs);
   in
     if ch
     then Syntax.const \<^syntax_const>\<open>_assign\<close> $ a $ b
     else syntax_const ctxt #Skip
   end;
 
 fun com_tr' ctxt (t,a) =
   let
     val (head, args) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb t);
     fun arg k = nth args (k - 1);
     val n = length args;
     val (_, args_a) = apfst (try (#1 o Term.dest_Const)) (Term.strip_comb a);
     fun arg_a k = nth args_a (k - 1)
   in
     case head of
       NONE => t
     | SOME c =>
         if c = const_syntax ctxt #Basic andalso n = 1 andalso is_f (arg 1) then
           mk_assign ctxt (arg 1)
         else if c = const_syntax ctxt #Seq andalso n = 2 then
           Syntax.const \<^syntax_const>\<open>_Seq\<close>
             $ com_tr' ctxt (arg 1, arg_a 1) $ com_tr' ctxt (arg 2, arg_a 2)
         else if c = const_syntax ctxt #Cond andalso n = 3 then
           Syntax.const \<^syntax_const>\<open>_Cond\<close> $
             bexp_tr' (arg 1) $ com_tr' ctxt (arg 2, arg_a 1) $ com_tr' ctxt (arg 3, arg_a 2)
         else if c = const_syntax ctxt #While andalso n = 2 then
                let val (xo,a') = case arg_a 3 of
                      Abs(x,_,a) => (if loose_bvar1(a,0) then SOME x else NONE,
                                     subst_bound (Syntax.free x, a)) |
                      t => (NONE,t)
                in Syntax.const \<^syntax_const>\<open>_While\<close>
                  $ bexp_tr' (arg 1) $ assn_tr' (arg_a 1) $ var_tr' xo (arg_a 2) $ com_tr' ctxt (arg 2, a')
                end
         else t
   end;
 
 in
 
 fun spec_tr' syn ctxt [p, c, a, q] =
   Syntax.const syn $ assn_tr' p $ com_tr' ctxt (c,a) $ assn_tr' q;
 
 end;
 
 
 (** setup **)
 
 val _ =
   Theory.setup
    (Sign.parse_translation
     [(\<^syntax_const>\<open>_hoare_vars\<close>, hoare_vars_tr),
      (\<^syntax_const>\<open>_hoare_vars_tc\<close>, hoare_tc_vars_tr)]);
 
 fun setup consts =
   Data.put (SOME consts) #>
   Sign.print_translation
    [(#Valid consts, spec_tr' \<^syntax_const>\<open>_hoare\<close>),
     (#ValidTC consts, spec_tr' \<^syntax_const>\<open>_hoare_tc\<close>)];
 
 end;