src/Pure/Isar/proof_context.ML
changeset 26435 bdce320cd426
parent 26393 42febbed5460
child 26463 9283b4185fdf
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:12 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 27 15:32:15 2008 +0100
     1.3 @@ -571,7 +571,7 @@
     1.4  fun standard_term_uncheck ctxt =
     1.5    map (contract_abbrevs ctxt);
     1.6  
     1.7 -fun add eq what f = Context.add_setup
     1.8 +fun add eq what f = Context.>>
     1.9    (Context.theory_map (what (fn xs => fn ctxt =>
    1.10      let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
    1.11  
    1.12 @@ -922,7 +922,7 @@
    1.13  
    1.14  in
    1.15  
    1.16 -val _ = Context.add_setup
    1.17 +val _ = Context.>>
    1.18   (Sign.add_syntax
    1.19     [("_context_const", "id => 'a", Delimfix "CONST _"),
    1.20      ("_context_const", "longid => 'a", Delimfix "CONST _"),