# HG changeset patch
# User wenzelm
# Date 1247692317 -7200
# Node ID fd3c60ad9155618c97fb91975bac1220377a2d6f
# Parent  fa0cc3c8f73d5e38e7866d8bea540d3b1fbc0cc0
eliminated obsolete legacy_varify;

diff -r fa0cc3c8f73d -r fd3c60ad9155 src/Pure/Isar/theory_target.ML
--- 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 ?