src/HOL/Tools/Meson/meson_clausify.ML
changeset 56245 84fc7dfa3cd4
parent 55523 9429e7b5b827
child 56811 b66639331db5
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -242,7 +242,7 @@
     1.4      fun aux (cluster as (cluster_no, cluster_skolem)) index_no pos t =
     1.5        case t of
     1.6          (t1 as Const (s, _)) $ Abs (s', T, t') =>
     1.7 -        if s = @{const_name all} orelse s = @{const_name All} orelse
     1.8 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
     1.9             s = @{const_name Ex} then
    1.10            let
    1.11              val skolem = (pos = (s = @{const_name Ex}))
    1.12 @@ -254,7 +254,7 @@
    1.13          else
    1.14            t
    1.15        | (t1 as Const (s, _)) $ t2 $ t3 =>
    1.16 -        if s = @{const_name "==>"} orelse s = @{const_name HOL.implies} then
    1.17 +        if s = @{const_name Pure.imp} orelse s = @{const_name HOL.implies} then
    1.18            t1 $ aux cluster index_no (not pos) t2 $ aux cluster index_no pos t3
    1.19          else if s = @{const_name HOL.conj} orelse
    1.20                  s = @{const_name HOL.disj} then
    1.21 @@ -275,13 +275,13 @@
    1.22    ct
    1.23    |> (case term_of ct of
    1.24          Const (s, _) $ Abs (s', _, _) =>
    1.25 -        if s = @{const_name all} orelse s = @{const_name All} orelse
    1.26 +        if s = @{const_name Pure.all} orelse s = @{const_name All} orelse
    1.27             s = @{const_name Ex} then
    1.28            Thm.dest_comb #> snd #> Thm.dest_abs (SOME s') #> snd #> zap pos
    1.29          else
    1.30            Conv.all_conv
    1.31        | Const (s, _) $ _ $ _ =>
    1.32 -        if s = @{const_name "==>"} orelse s = @{const_name implies} then
    1.33 +        if s = @{const_name Pure.imp} orelse s = @{const_name implies} then
    1.34            Conv.combination_conv (Conv.arg_conv (zap (not pos))) (zap pos)
    1.35          else if s = @{const_name conj} orelse s = @{const_name disj} then
    1.36            Conv.combination_conv (Conv.arg_conv (zap pos)) (zap pos)