prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
authorwenzelm
Sat Feb 01 20:46:19 2014 +0100 (2014-02-01)
changeset 552371e341728bae9
parent 55236 8d61b0aa7a0d
child 55238 7ddb889e23bd
child 55239 97921d23ebe3
prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
src/Tools/adhoc_overloading.ML
     1.1 --- a/src/Tools/adhoc_overloading.ML	Sat Feb 01 18:42:46 2014 +0100
     1.2 +++ b/src/Tools/adhoc_overloading.ML	Sat Feb 01 20:46:19 2014 +0100
     1.3 @@ -172,7 +172,7 @@
     1.4        |> get_overloaded ctxt
     1.5        |> Option.map (Const o rpair (Term.type_of t));
     1.6    in
     1.7 -    Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc]
     1.8 +    Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
     1.9    end;
    1.10  
    1.11  fun check ctxt =