--- 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'))