src/HOL/Tools/Predicate_Compile/pred_compile_data.ML

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -132,7 +132,7 @@
     val th = th
       |> inline_equations thy
       |> Pred_Compile_Set.unfold_set_notation
-      (*  |> AxClass.unoverload thy *)
+      |> AxClass.unoverload thy
     val (const, th) =
       if is_equationlike th then
         let