src/Pure/Isar/proof_context.ML
changeset 25060 17c313217998
parent 25052 a014d544f54d
child 25063 8e702c7adc34
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:56 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 19:45:57 2007 +0200
     1.3 @@ -585,16 +585,17 @@
     1.4  fun standard_term_uncheck ctxt =
     1.5    map (contract_abbrevs ctxt);
     1.6  
     1.7 -fun add what f = Context.add_setup
     1.8 -  (Context.theory_map (what (fn xs => fn ctxt => (f ctxt xs, ctxt))));
     1.9 +fun add eq what f = Context.add_setup
    1.10 +  (Context.theory_map (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 -val _ = add (Syntax.add_typ_check 0 "standard") standard_typ_check;
    1.16 -val _ = add (Syntax.add_term_check 0 "standard") standard_term_check;
    1.17 -val _ = add (Syntax.add_term_check 100 "fixate") prepare_patterns;
    1.18 +val _ = add (op =) (Syntax.add_typ_check 0 "standard") standard_typ_check;
    1.19 +val _ = add (op aconv) (Syntax.add_term_check 0 "standard") standard_term_check;
    1.20 +val _ = add (op aconv) (Syntax.add_term_check 100 "fixate") prepare_patterns;
    1.21  
    1.22 -val _ = add (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
    1.23 +val _ = add (op aconv) (Syntax.add_term_uncheck 0 "standard") standard_term_uncheck;
    1.24  
    1.25  end;
    1.26