src/Pure/conv.ML
changeset 56245 84fc7dfa3cd4
parent 50639 f1c2f911ae33
child 59586 ddf6deaadfe8
     1.1 --- a/src/Pure/conv.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Pure/conv.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -140,17 +140,17 @@
     1.4  
     1.5  fun forall_conv cv ctxt ct =
     1.6    (case Thm.term_of ct of
     1.7 -    Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
     1.8 +    Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
     1.9    | _ => raise CTERM ("forall_conv", [ct]));
    1.10  
    1.11  fun implies_conv cv1 cv2 ct =
    1.12    (case Thm.term_of ct of
    1.13 -    Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
    1.14 +    Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
    1.15    | _ => raise CTERM ("implies_conv", [ct]));
    1.16  
    1.17  fun implies_concl_conv cv ct =
    1.18    (case Thm.term_of ct of
    1.19 -    Const ("==>", _) $ _ $ _ => arg_conv cv ct
    1.20 +    Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
    1.21    | _ => raise CTERM ("implies_concl_conv", [ct]));
    1.22  
    1.23