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.mode_abbrev;
authorwenzelm
Sat, 22 Sep 2007 17:45:58 +0200
changeset 24676 63eaef3207e1
parent 24675 2be1253a20d3
child 24677 c6295d2dce48
ProofContext.mode_abbrev;
src/Pure/Isar/specification.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/specification.ML	Sat Sep 22 17:45:57 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Sep 22 17:45:58 2007 +0200
@@ -147,7 +147,7 @@
   let
     val ((vars, [(_, [prop])]), _) =
       prep (the_list raw_var) [(("", []), [raw_prop])]
-        (lthy |> ProofContext.set_expand_abbrevs false);
+        (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
     val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
     val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
       if x = y then mx
isabelle