--- a/src/HOL/Hoare/Hoare.thy Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Hoare/Hoare.thy Thu Mar 05 08:23:11 2009 +0100
@@ -161,9 +161,9 @@
(* assn_tr' & bexp_tr'*)
ML{*
fun assn_tr' (Const ("Collect",_) $ T) = dest_abstuple T
- | assn_tr' (Const ("op Int",_) $ (Const ("Collect",_) $ T1) $
+ | assn_tr' (Const (@{const_name Set.Int}, _) $ (Const ("Collect",_) $ T1) $
(Const ("Collect",_) $ T2)) =
- Syntax.const "op Int" $ dest_abstuple T1 $ dest_abstuple T2
+ Syntax.const "Set.Int" $ dest_abstuple T1 $ dest_abstuple T2
| assn_tr' t = t;
fun bexp_tr' (Const ("Collect",_) $ T) = dest_abstuple T