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.
LocalDefs.def_export;
authorwenzelm
Sat, 28 Jan 2006 17:28:51 +0100
changeset 18817 ad8bc3e55aa3
parent 18816 aebd7f315b92
child 18818 86eec44dae66
LocalDefs.def_export;
src/HOL/Tools/meson.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/meson.ML	Sat Jan 28 17:28:50 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Sat Jan 28 17:28:51 2006 +0100
@@ -441,7 +441,7 @@
 (*Expand all definitions (presumably of Skolem functions) in a proof state.*)
 fun expand_defs_tac st =
   let val defs = filter (can dest_equals) (#hyps (crep_thm st))
-  in  ProofContext.def_export false defs st  end;
+  in  LocalDefs.def_export false defs st  end;
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions*)
 fun MESON cltac i st =
isabelle