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.
ProofContext.abbrev_mode;
authorwenzelm
Thu, 19 Jun 2008 22:05:04 +0200
changeset 27285 def40a211768
parent 27284 2ddb6a2db65c
child 27286 2ea20e5fdf16
ProofContext.abbrev_mode;
src/Pure/Isar/overloading.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/overloading.ML	Thu Jun 19 22:05:01 2008 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Jun 19 22:05:04 2008 +0200
@@ -70,7 +70,7 @@
     val { primary_constraints, secondary_constraints, improve, subst,
       consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
     val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
-    val is_abbrev = consider_abbrevs andalso ProofContext.is_abbrev_mode ctxt;
+    val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt;
     val passed_or_abbrev = passed orelse is_abbrev;
     fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
          of SOME ty_ty' => Type.typ_match tsig ty_ty'
isabelle