src/FOLP/hypsubst.ML
changeset 56245 84fc7dfa3cd4
parent 42799 4e33894aec6d
child 60754 02924903a6fd
     1.1 --- a/src/FOLP/hypsubst.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/FOLP/hypsubst.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -58,8 +58,8 @@
     1.4     assumption.  Returns the number of intervening assumptions, paried with
     1.5     the rule asm_rl (resp. sym). *)
     1.6  fun eq_var bnd =
     1.7 -  let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t
     1.8 -        | eq_var_aux k (Const("==>",_) $ A $ B) =
     1.9 +  let fun eq_var_aux k (Const(@{const_name Pure.all},_) $ Abs(_,_,t)) = eq_var_aux k t
    1.10 +        | eq_var_aux k (Const(@{const_name Pure.imp},_) $ A $ B) =
    1.11                ((k, inspect_pair bnd (dest_eq A))
    1.12                        (*Exception Match comes from inspect_pair or dest_eq*)
    1.13                 handle Match => eq_var_aux (k+1) B)