# HG changeset patch
# User wenzelm
# Date 1293622473 -3600
# Node ID 3d99be274463699a23a468b8a6a1faf21b5bfb95
# Parent  0bc364f772efa19ccc55f336bca31fb793008cac
made SML/NJ happy;

diff -r 0bc364f772ef -r 3d99be274463 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Dec 29 12:25:22 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Dec 29 12:34:33 2010 +0100
@@ -34,7 +34,7 @@
 val intro_table = inductive_intro_table ctxt subst def_table
 val ground_thm_table = ground_theorem_table thy
 val ersatz_table = ersatz_table ctxt
-val hol_ctxt as {thy, ...} =
+val hol_ctxt as {thy, ...} : hol_context =
   {thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
    stds = stds, wfs = [], user_axioms = NONE, debug = false,
    whacks = [], binary_ints = SOME false, destroy_constrs = true,