src/FOLP/simp.ML
changeset 56245 84fc7dfa3cd4
parent 44121 44adaa6db327
child 58963 26bf09b95dda
     1.1 --- a/src/FOLP/simp.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -405,10 +405,10 @@
     1.4      else ();
     1.5  
     1.6  (* Skip the first n hyps of a goal, and return the rest in generalized form *)
     1.7 -fun strip_varify(Const("==>", _) $ H $ B, n, vs) =
     1.8 +fun strip_varify(Const(@{const_name Pure.imp}, _) $ H $ B, n, vs) =
     1.9          if n=0 then subst_bounds(vs,H)::strip_varify(B,0,vs)
    1.10          else strip_varify(B,n-1,vs)
    1.11 -  | strip_varify(Const("all",_)$Abs(_,T,t), n, vs) =
    1.12 +  | strip_varify(Const(@{const_name Pure.all},_)$Abs(_,T,t), n, vs) =
    1.13          strip_varify(t,n,Var(("?",length vs),T)::vs)
    1.14    | strip_varify  _  = [];
    1.15