# HG changeset patch
# User blanchet
# Date 1256551328 -3600
# Node ID 0183ab3ca7b4b66a0de449d77e1829fbd37c4f48
# Parent  e3d741e9d2feb15e8adb61d2bf1ecfb402dcda44
make Nitpick compile again

diff -r e3d741e9d2fe -r 0183ab3ca7b4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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 *)
diff -r e3d741e9d2fe -r 0183ab3ca7b4 src/HOL/Tools/Nitpick/nitpick_model.ML
--- 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)