Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
authorwenzelm
Sat, 01 Feb 2014 20:46:19 +0100
changeset 55237 1e341728bae9
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 file | annotate | diff | comparison | revisions 
--- a/src/Tools/adhoc_overloading.ML	Sat Feb 01 18:42:46 2014 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sat Feb 01 20:46:19 2014 +0100
@@ -172,7 +172,7 @@
       |> get_overloaded ctxt
       |> Option.map (Const o rpair (Term.type_of t));
   in
-    Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] [proc]
+    Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
   end;
 
 fun check ctxt =
isabelle