src/HOL/Tools/SMT/smt_replay_methods.ML

 fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
 
 fun abstract_ter abs f t t1 t2 t3 =
   abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f))
 
-fun abstract_lit (\<^const>\<open>HOL.Not\<close> $ t) = abstract_term t #>> HOLogic.mk_not
+fun abstract_lit \<^Const>\<open>Not for t\<close> = abstract_term t #>> HOLogic.mk_not
   | abstract_lit t = abstract_term t
 
-fun abstract_not abs (t as \<^const>\<open>HOL.Not\<close> $ t1) =
+fun abstract_not abs (t as \<^Const_>\<open>Not\<close> $ t1) =
       abstract_sub t (abs t1 #>> HOLogic.mk_not)
   | abstract_not _ t = abstract_lit t
 
-fun abstract_conj (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+fun abstract_conj (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
       abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
   | abstract_conj t = abstract_lit t
 
-fun abstract_disj (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+fun abstract_disj (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
       abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
   | abstract_disj t = abstract_lit t
 
-fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
+fun abstract_prop (t as (c as \<^Const>\<open>If \<^Type>\<open>bool\<close>\<close>) $ t1 $ t2 $ t3) =
       abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
-  | abstract_prop (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
-  | abstract_prop (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>conj\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
-  | abstract_prop (t as \<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>implies\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
-  | abstract_prop (t as \<^term>\<open>HOL.eq :: bool => _\<close> $ t1 $ t2) =
+  | abstract_prop (t as \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close>\<close> $ t1 $ t2) =
       abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
   | abstract_prop t = abstract_not abstract_prop t
 
 fun abstract_arith ctxt u =
   let

           abstract_sub t (abstract_term t)
       | abs (t as (c as Const _) $ Abs (s, T, t')) =
           abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
       | abs (t as (c as Const (\<^const_name>\<open>If\<close>, _)) $ t1 $ t2 $ t3) =
           abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
-      | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
-      | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+      | abs (t as \<^Const_>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+      | abs (t as \<^Const_>\<open>disj\<close> $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
       | abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
           abstract_sub t (abs t1 #>> (fn u => c $ u))
       | abs (t as (c as Const (\<^const_name>\<open>plus_class.plus\<close>, _)) $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))

             (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
               (SOME u, cx') => (u, cx')
             | (NONE, _) => abstract_term t cx))
   in abs u end
 
-fun abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t1 $ t2))) =
+fun abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>disj for t1 t2\<close>\<close>) =
       abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
         HOLogic.mk_not o HOLogic.mk_disj)
-  | abstract_unit (t as (\<^const>\<open>HOL.disj\<close> $ t1 $ t2)) =
+  | abstract_unit (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
         HOLogic.mk_disj)
   | abstract_unit (t as (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) =
       if fastype_of t1 = \<^typ>\<open>bool\<close> then
         abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2))) =
+  | abstract_unit (t as \<^Const_>\<open>Not for \<^Const_>\<open>HOL.eq _ for t1 t2\<close>\<close>) =
       if fastype_of t1 = \<^typ>\<open>bool\<close> then
         abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
           HOLogic.mk_eq #>> HOLogic.mk_not)
       else abstract_lit t
-  | abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ t1)) =
+  | abstract_unit (t as \<^Const>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not)
   | abstract_unit t = abstract_lit t
 
-fun abstract_bool (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool (t as (@{const HOL.conj} $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const_>\<open>conj for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_conj)
-  | abstract_bool (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
       if fastype_of t1 = @{typ bool} then
         abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_bool (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool t1 #>> HOLogic.mk_not)
-  | abstract_bool (t as (@{const HOL.implies} $ t1 $ t2)) =
+  | abstract_bool (t as \<^Const>\<open>implies for t1 t2\<close>) =
       abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>>
         HOLogic.mk_imp)
   | abstract_bool t = abstract_lit t
 
-fun abstract_bool_shallow (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool_shallow t1 ##>> abstract_bool_shallow t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool_shallow (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool_shallow (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool_shallow t1 #>> HOLogic.mk_not)
   | abstract_bool_shallow t = abstract_term t
 
-fun abstract_bool_shallow_equivalence (t as (@{const HOL.disj} $ t1 $ t2)) =
+fun abstract_bool_shallow_equivalence (t as \<^Const_>\<open>disj for t1 t2\<close>) =
       abstract_sub t (abstract_bool_shallow_equivalence t1 ##>> abstract_bool_shallow_equivalence t2 #>>
         HOLogic.mk_disj)
-  | abstract_bool_shallow_equivalence (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) =
-      if fastype_of t1 = @{typ bool} then
+  | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>HOL.eq _ for t1 t2\<close>) =
+      if fastype_of t1 = \<^Type>\<open>bool\<close> then
         abstract_sub t (abstract_lit t1 ##>> abstract_lit t2 #>>
           HOLogic.mk_eq)
       else abstract_lit t
-  | abstract_bool_shallow_equivalence (t as (@{const HOL.Not} $ t1)) =
+  | abstract_bool_shallow_equivalence (t as \<^Const_>\<open>Not for t1\<close>) =
       abstract_sub t (abstract_bool_shallow_equivalence t1 #>> HOLogic.mk_not)
   | abstract_bool_shallow_equivalence t = abstract_lit t
 
 fun abstract_arith_shallow ctxt u =
   let

           abstract_sub t (abstract_term t)
       | abs (t as (c as Const _) $ Abs (s, T, t')) =
           abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
       | abs (t as (Const (\<^const_name>\<open>If\<close>, _)) $ _ $ _ $ _) =
           abstract_sub t (abstract_term t)
-      | abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
-      | abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
+      | abs (t as \<^Const>\<open>Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
+      | abs (t as \<^Const>\<open>disj\<close> $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
       | abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) =
           abstract_sub t (abs t1 #>> (fn u => c $ u))
       | abs (t as (c as Const (\<^const_name>\<open>plus_class.plus\<close>, _)) $ t1 $ t2) =
           abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))