1.1 --- a/src/HOL/Prolog/prolog.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Prolog/prolog.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  fun isD t = case t of
     1.5      Const(@{const_name Trueprop},_)$t     => isD t
     1.6    | Const(@{const_name "op &"}  ,_)$l$r     => isD l andalso isD r
     1.7 -  | Const(@{const_name "op -->"},_)$l$r     => isG l andalso isD r
     1.8 +  | Const(@{const_name HOL.implies},_)$l$r     => isG l andalso isD r
     1.9    | Const(   "==>",_)$l$r     => isG l andalso isD r
    1.10    | Const(@{const_name All},_)$Abs(s,_,t) => isD t
    1.11    | Const("all",_)$Abs(s,_,t) => isD t
    1.12 @@ -32,7 +32,7 @@
    1.13      Const(@{const_name Trueprop},_)$t     => isG t
    1.14    | Const(@{const_name "op &"}  ,_)$l$r     => isG l andalso isG r
    1.15    | Const(@{const_name "op |"}  ,_)$l$r     => isG l andalso isG r
    1.16 -  | Const(@{const_name "op -->"},_)$l$r     => isD l andalso isG r
    1.17 +  | Const(@{const_name HOL.implies},_)$l$r     => isD l andalso isG r
    1.18    | Const(   "==>",_)$l$r     => isD l andalso isG r
    1.19    | Const(@{const_name All},_)$Abs(_,_,t) => isG t
    1.20    | Const("all",_)$Abs(_,_,t) => isG t
    1.21 @@ -54,7 +54,7 @@
    1.22        _$(Const(@{const_name All} ,_)$Abs(s,_,_))=> at(thm RS
    1.23          (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec))
    1.24      | _$(Const(@{const_name "op &"},_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    1.25 -    | _$(Const(@{const_name "op -->"},_)$_$_)     => at(thm RS mp)
    1.26 +    | _$(Const(@{const_name HOL.implies},_)$_$_)     => at(thm RS mp)
    1.27      | _                             => [thm]
    1.28  in map zero_var_indexes (at thm) end;
    1.29  
    1.30 @@ -72,7 +72,7 @@
    1.31    -- is nice, but cannot instantiate unknowns in the assumptions *)
    1.32  fun hyp_resolve_tac i st = let
    1.33          fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a  ,t))
    1.34 -        |   ap (Const(@{const_name "op -->"},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    1.35 +        |   ap (Const(@{const_name HOL.implies},_)$_$t)    =(case ap t of (k,_,t) => (k,true ,t))
    1.36          |   ap t                          =                         (0,false,t);
    1.37  (*
    1.38          fun rep_goal (Const ("all",_)$Abs (_,_,t)) = rep_goal t