src/HOL/Hoare/hoare_tac.ML
changeset 37677 c5a8b612e571
parent 37591 d3daea901123
child 38012 3ca193a6ae5a
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    | abs2list _ = [];
     1.5  
     1.6  (** maps {(x1,...,xn). t} to [x1,...,xn] **)
     1.7 -fun mk_vars (Const ("Collect",_) $ T) = abs2list T
     1.8 +fun mk_vars (Const (@{const_name Collect},_) $ T) = abs2list T
     1.9    | mk_vars _ = [];
    1.10  
    1.11  (** abstraction of body over a tuple formed from a list of free variables.