12 begin |
12 begin |
13 |
13 |
14 ML {* |
14 ML {* |
15 exception FAIL |
15 exception FAIL |
16 |
16 |
17 val defs = Nitpick_HOL.all_axioms_of @{theory} |> #1 |
17 val subst = [] |
18 val def_table = Nitpick_HOL.const_def_table @{context} defs |
18 val defs = Nitpick_HOL.all_axioms_of @{theory} subst |> #1 |
|
19 val def_table = Nitpick_HOL.const_def_table @{context} subst defs |
19 val hol_ctxt : Nitpick_HOL.hol_context = |
20 val hol_ctxt : Nitpick_HOL.hol_context = |
20 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
21 {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [], |
21 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, |
22 stds = [(NONE, true)], wfs = [], user_axioms = NONE, debug = false, |
22 binary_ints = SOME false, destroy_constrs = false, specialize = false, |
23 binary_ints = SOME false, destroy_constrs = false, specialize = false, |
23 skolemize = false, star_linear_preds = false, uncurry = false, |
24 skolemize = false, star_linear_preds = false, uncurry = false, |