# HG changeset patch # User wenzelm # Date 1332075594 -3600 # Node ID 8b13ebf3eda4ecb73df4eda3f7fd888c053b0f75 # Parent 0dacedb4a94820982e1b14ee1530862d664151ff comment; diff -r 0dacedb4a948 -r 8b13ebf3eda4 src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Mar 18 13:51:51 2012 +0100 +++ b/src/Pure/sign.ML Sun Mar 18 13:59:54 2012 +0100 @@ -420,7 +420,7 @@ (* abbreviations *) -fun add_abbrev mode (b, raw_t) thy = +fun add_abbrev mode (b, raw_t) thy = (* FIXME proper ctxt (?) *) let val ctxt = Syntax.init_pretty_global thy; val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;