adapt example
authorblanchet
Tue, 01 Jun 2010 17:04:21 +0200
changeset 37268 8ad1e3768b4f
parent 37267 5c47d633c84d
child 37269 49c45156c9e1
adapt example
src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Jun 01 16:17:46 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Jun 01 17:04:21 2010 +0200
@@ -15,7 +15,7 @@
 exception FAIL
 
 val subst = []
-val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1
+val defs = Nitpick_HOL.all_axioms_of @{context} subst |> #1
 val def_table = Nitpick_HOL.const_def_table @{context} subst defs
 val hol_ctxt : Nitpick_HOL.hol_context =
   {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],