src/HOL/Tools/SMT/z3_proof_tools.ML

       | @{term Not} $ _ => abstr1 cvs ct
       | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
       | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
       | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
-      | Const (@{const_name distinct}, _) $ _ =>
+      | Const (@{const_name SMT.distinct}, _) $ _ =>
           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
           else fresh_abstraction cvs ct
       | Const (@{const_name If}, _) $ _ $ _ $ _ =>
           if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
       | Const (@{const_name All}, _) $ _ =>

 
   fun set_conv ct =
     (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
     (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
 
-  val dist1 = @{lemma "distinct [] == ~False" by simp}
-  val dist2 = @{lemma "distinct [x] == ~False" by simp}
-  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
-    by simp}
+  val dist1 = @{lemma "SMT.distinct [] == ~False" by (simp add: distinct_def)}
+  val dist2 = @{lemma "SMT.distinct [x] == ~False" by (simp add: distinct_def)}
+  val dist3 = @{lemma "SMT.distinct (x # xs) == x ~: set xs & distinct xs"
+    by (simp add: distinct_def)}
 
   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
 in
 fun unfold_distinct_conv ct =
   (Conv.rewrs_conv [dist1, dist2] else_conv