--- a/src/HOL/Isar_Examples/Hoare.thy Sat Mar 26 10:52:29 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Sat Mar 26 12:01:40 2011 +0100
@@ -237,15 +237,9 @@
quote_tr' (Syntax.const name) (t :: ts)
| bexp_tr' _ _ = raise Match;
- fun K_tr' (Abs (_, _, t)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' (Abs (_, _, Abs (_, _, t) $ Bound 0)) =
- if null (loose_bnos t) then t else raise Match
- | K_tr' _ = raise Match;
-
fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
- (Abs (x, dummyT, K_tr' k) :: ts)
+ (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
| assign_tr' _ = raise Match;
in
[(@{const_syntax Collect}, assert_tr'),