changeset 47008 | 8b13ebf3eda4 |
parent 47006 | 5ee8004e2151 |
child 52143 | 36ffe23b25f8 |
--- 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;