src/Pure/Isar/proof_context.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 26673 cda3df424bad
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -571,9 +571,8 @@
     1.4  fun standard_term_uncheck ctxt =
     1.5    map (contract_abbrevs ctxt);
     1.6  
     1.7 -fun add eq what f = Context.>>
     1.8 -  (Context.theory_map (what (fn xs => fn ctxt =>
     1.9 -    let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end)));
    1.10 +fun add eq what f = Context.>> (what (fn xs => fn ctxt =>
    1.11 +  let val xs' = f ctxt xs in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end));
    1.12  
    1.13  in
    1.14  
    1.15 @@ -922,14 +921,14 @@
    1.16  
    1.17  in
    1.18  
    1.19 -val _ = Context.>>
    1.20 +val _ = Context.>> (Context.map_theory
    1.21   (Sign.add_syntax
    1.22     [("_context_const", "id => 'a", Delimfix "CONST _"),
    1.23      ("_context_const", "longid => 'a", Delimfix "CONST _"),
    1.24      ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
    1.25      ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
    1.26    Sign.add_advanced_trfuns
    1.27 -    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
    1.28 +    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
    1.29  
    1.30  end;
    1.31