diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -108,7 +108,7 @@
       val def = Logic.mk_equals (lhs, atom)
       val ([definition], thy') = thy
         |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-        |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+        |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
     in
       (lhs, ((full_constname, [definition]) :: defs, thy'))
     end
@@ -327,7 +327,7 @@
             val def = Logic.mk_equals (lhs, abs_arg')
             val ([definition], thy') = thy
               |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-              |> PureThy.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
+              |> Global_Theory.add_defs false [((Binding.name (constname ^ "_def"), def), [])]
           in
             (list_comb (Logic.varify_global const, vars),
               ((full_constname, [definition])::new_defs, thy'))