--- a/src/Pure/conv.ML Fri Mar 21 15:12:03 2014 +0100
+++ b/src/Pure/conv.ML Fri Mar 21 20:33:56 2014 +0100
@@ -140,17 +140,17 @@
fun forall_conv cv ctxt ct =
(case Thm.term_of ct of
- Const ("all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
+ Const ("Pure.all", _) $ Abs _ => arg_conv (abs_conv cv ctxt) ct
| _ => raise CTERM ("forall_conv", [ct]));
fun implies_conv cv1 cv2 ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
+ Const ("Pure.imp", _) $ _ $ _ => combination_conv (arg_conv cv1) cv2 ct
| _ => raise CTERM ("implies_conv", [ct]));
fun implies_concl_conv cv ct =
(case Thm.term_of ct of
- Const ("==>", _) $ _ $ _ => arg_conv cv ct
+ Const ("Pure.imp", _) $ _ $ _ => arg_conv cv ct
| _ => raise CTERM ("implies_concl_conv", [ct]));