made SML/NJ happy;
authorwenzelm
Wed Dec 29 12:34:33 2010 +0100 (2010-12-29)
changeset 414103d99be274463
parent 41409 0bc364f772ef
child 41411 3bcc3b9e1020
made SML/NJ happy;
src/HOL/Nitpick_Examples/Mono_Nits.thy
     1.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Dec 29 12:25:22 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Dec 29 12:34:33 2010 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  val intro_table = inductive_intro_table ctxt subst def_table
     1.5  val ground_thm_table = ground_theorem_table thy
     1.6  val ersatz_table = ersatz_table ctxt
     1.7 -val hol_ctxt as {thy, ...} =
     1.8 +val hol_ctxt as {thy, ...} : hol_context =
     1.9    {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
    1.10     stds = stds, wfs = [], user_axioms = NONE, debug = false,
    1.11     whacks = [], binary_ints = SOME false, destroy_constrs = true,