src/HOL/Tools/SMT/z3_isar.ML
changeset 69593 3dda49e08b9d
parent 60924 610794dff23c
     1.1 --- a/src/HOL/Tools/SMT/z3_isar.ML	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_isar.ML	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4            end
     1.5        end
     1.6  
     1.7 -fun dest_alls (Const (@{const_name Pure.all}, _) $ Abs (abs as (_, T, _))) =
     1.8 +fun dest_alls (Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs (abs as (_, T, _))) =
     1.9      let val (s', t') = Term.dest_abs abs in
    1.10        dest_alls t' |>> cons (s', T)
    1.11      end