make Nitpick compile again
authorblanchet
Mon Oct 26 11:02:08 2009 +0100 (2009-10-26)
changeset 332020183ab3ca7b4
parent 33201 e3d741e9d2fe
child 33203 322d928d9f8f
make Nitpick compile again
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 26 09:14:29 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 26 11:02:08 2009 +0100
     1.3 @@ -1632,7 +1632,7 @@
     1.4  val cached_wf_props : (term * bool) list Unsynchronized.ref =
     1.5    Unsynchronized.ref []
     1.6  
     1.7 -val termination_tacs = [LexicographicOrder.lex_order_tac,
     1.8 +val termination_tacs = [Lexicographic_Order.lex_order_tac,
     1.9                          ScnpReconstruct.sizechange_tac]
    1.10  
    1.11  (* extended_context -> const_table -> styp -> bool *)
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 26 09:14:29 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 26 11:02:08 2009 +0100
     2.3 @@ -478,17 +478,17 @@
     2.4      val name_of = fst o dest_Const
     2.5      val thy = ProofContext.theory_of ctxt |> Context.reject_draft
     2.6      val (maybe_t, thy) =
     2.7 -      Sign.declare_const [] ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
     2.8 -                             Mixfix (maybe_mixfix, [1000], 1000)) thy
     2.9 +      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    2.10 +                          Mixfix (maybe_mixfix, [1000], 1000)) thy
    2.11      val (base_t, thy) =
    2.12 -      Sign.declare_const [] ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    2.13 -                             Mixfix (base_mixfix, [1000], 1000)) thy
    2.14 +      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
    2.15 +                          Mixfix (base_mixfix, [1000], 1000)) thy
    2.16      val (step_t, thy) =
    2.17 -      Sign.declare_const [] ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    2.18 -                             Mixfix (step_mixfix, [1000], 1000)) thy
    2.19 +      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
    2.20 +                          Mixfix (step_mixfix, [1000], 1000)) thy
    2.21      val (abs_t, thy) =
    2.22 -      Sign.declare_const [] ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    2.23 -                             Mixfix (abs_mixfix, [40], 40)) thy
    2.24 +      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
    2.25 +                          Mixfix (abs_mixfix, [40], 40)) thy
    2.26    in
    2.27      ((name_of maybe_t, name_of base_t, name_of step_t, name_of abs_t),
    2.28       ProofContext.transfer_syntax thy ctxt)