--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 26 09:14:29 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 26 11:02:08 2009 +0100
@@ -1632,7 +1632,7 @@
val cached_wf_props : (term * bool) list Unsynchronized.ref =
Unsynchronized.ref []
-val termination_tacs = [LexicographicOrder.lex_order_tac,
+val termination_tacs = [Lexicographic_Order.lex_order_tac,
ScnpReconstruct.sizechange_tac]
(* extended_context -> const_table -> styp -> bool *)
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Oct 26 09:14:29 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Oct 26 11:02:08 2009 +0100
@@ -478,17 +478,17 @@
val name_of = fst o dest_Const
val thy = ProofContext.theory_of ctxt |> Context.reject_draft
val (maybe_t, thy) =
- Sign.declare_const [] ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
- Mixfix (maybe_mixfix, [1000], 1000)) thy
+ Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
+ Mixfix (maybe_mixfix, [1000], 1000)) thy
val (base_t, thy) =
- Sign.declare_const [] ((@{binding nitpick_base}, @{typ "'a => 'a"}),
- Mixfix (base_mixfix, [1000], 1000)) thy
+ Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
+ Mixfix (base_mixfix, [1000], 1000)) thy
val (step_t, thy) =
- Sign.declare_const [] ((@{binding nitpick_step}, @{typ "'a => 'a"}),
- Mixfix (step_mixfix, [1000], 1000)) thy
+ Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
+ Mixfix (step_mixfix, [1000], 1000)) thy
val (abs_t, thy) =
- Sign.declare_const [] ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
- Mixfix (abs_mixfix, [40], 40)) thy
+ Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
+ Mixfix (abs_mixfix, [40], 40)) thy
in
((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
ProofContext.transfer_syntax thy ctxt)