--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Aug 26 13:09:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Aug 26 15:48:08 2010 +0200
@@ -176,9 +176,9 @@
val t = Const (const, T)
val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
in
- if (is_inductify options) then
+ if is_inductify options then
let
- val lthy' = Local_Theory.theory (preprocess options t) lthy
+ val lthy' = Local_Theory.background_theory (preprocess options t) lthy
val const =
case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
SOME c => c