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.
PrimitiveDefs.dest/abs_def;
authorwenzelm
Tue, 14 Aug 2007 13:20:19 +0200
changeset 24261 dd31811bdf46
parent 24260 d68040094415
child 24262 6d9b1157b9ab
PrimitiveDefs.dest/abs_def;
src/Pure/Isar/local_defs.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/local_defs.ML	Tue Aug 14 13:20:18 2007 +0200
+++ b/src/Pure/Isar/local_defs.ML	Tue Aug 14 13:20:19 2007 +0200
@@ -45,11 +45,11 @@
     fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^ display_term eq);
     val ((lhs, _), eq') = eq
       |> Sign.no_vars pp
-      |> Logic.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
+      |> PrimitiveDefs.dest_def pp Term.is_Free (Variable.is_fixed ctxt) (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
-val abs_def = Logic.abs_def #>> Term.dest_Free;
+val abs_def = PrimitiveDefs.abs_def #>> Term.dest_Free;
 
 fun mk_def ctxt args =
   let
isabelle