--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Oct 31 11:23:21 2012 +0100
@@ -1311,10 +1311,10 @@
|> map snd
end
-(* Ideally we would check against "Complex_Main", not "Refute", but any theory
- will do as long as it contains all the "axioms" and "axiomatization"
+(* Ideally we would check against "Complex_Main", not "Hilbert_Choice", but any
+ theory will do as long as it contains all the "axioms" and "axiomatization"
commands. *)
-fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
+fun is_built_in_theory thy = Theory.subthy (thy, @{theory Hilbert_Choice})
fun all_nondefs_of ctxt subst =
ctxt |> Spec_Rules.get