src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 52696 38466f4f3483
parent 52174 7fd0b5cfbb79
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Jul 17 23:51:10 2013 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jul 18 13:12:54 2013 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  fun add_wacky_syntax ctxt =
     1.5    let
     1.6      val name_of = fst o dest_Const
     1.7 -    val thy = Proof_Context.theory_of ctxt |> Context.reject_draft
     1.8 +    val thy = Proof_Context.theory_of ctxt
     1.9      val (maybe_t, thy) =
    1.10        Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    1.11                            Mixfix (maybe_mixfix (), [1000], 1000)) thy