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.
eliminated obsolete legacy_varify;
authorwenzelm
Wed, 15 Jul 2009 23:11:57 +0200
changeset 32009 fd3c60ad9155
parent 32008 fa0cc3c8f73d
child 32010 cb1a1c94b4cd
eliminated obsolete legacy_varify;
src/Pure/Isar/theory_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/theory_target.ML	Wed Jul 15 21:42:24 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Jul 15 23:11:57 2009 +0200
@@ -177,7 +177,6 @@
   let
     val b' = Morphism.binding phi b;
     val rhs' = Morphism.term phi rhs;
-    val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
     val arg = (b', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
@@ -188,7 +187,7 @@
   in
     not (is_class andalso (similar_body orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
+        (Sign.add_abbrev PrintMode.internal tags arg)
         (ProofContext.add_abbrev PrintMode.internal tags arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           similar_body ?
isabelle