src/Pure/Isar/locale.ML

       | items prfx (x :: xs) = Pretty.block [Pretty.str prfx, Pretty.brk 1, x] :: items "  and" xs;
     fun prt_elem (Fixes fixes) = items "fixes" (map prt_fix fixes)
       | prt_elem (Constrains csts) = items "constrains" (map prt_cst csts)
       | prt_elem (Assumes asms) = items "assumes" (map prt_asm asms)
       | prt_elem (Defines defs) = items "defines" (map prt_def defs)
-      | prt_elem (Notes facts) =
-        if show_facts then items "notes" (map prt_note facts) else [];
+      | prt_elem (Notes facts) = items "notes" (map prt_note facts);
   in
-    Pretty.big_list "context elements:" (map (Pretty.chunks o prt_elem) all_elems)
+    Pretty.big_list "context elements:" (all_elems
+      |> (if show_facts then I else filter (fn Notes _ => false | _ => true))
+      |> map (Pretty.chunks o prt_elem))
     |> Pretty.writeln
   end;
 
 
 

     fun add_def ((inst, tinst), (p, pT)) =
       let
         val (t, T) = case find_first (fn (Free (a, _), _) => a = p) defs of
                NONE => error ("Instance missing for parameter " ^ quote p)
              | SOME (Free (_, T), t) => (t, T);
-        val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
+        val d = inst_tab_term (inst, tinst) t;
       in (Symtab.curried_update_new (p, d) inst, tinst) end;
     val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
     (* Note: inst and tinst contain no vars. *)
 
     (** compute proof obligations **)