1.1 --- a/src/Pure/sign.ML	Sun Mar 18 13:51:51 2012 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Mar 18 13:59:54 2012 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4  
     1.5  (* abbreviations *)
     1.6  
     1.7 -fun add_abbrev mode (b, raw_t) thy =
     1.8 +fun add_abbrev mode (b, raw_t) thy =  (* FIXME proper ctxt (?) *)
     1.9    let
    1.10      val ctxt = Syntax.init_pretty_global thy;
    1.11      val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;