eliminated obsolete legacy_varify;
authorwenzelm
Wed Jul 15 23:11:57 2009 +0200 (2009-07-15)
changeset 32009fd3c60ad9155
parent 32008 fa0cc3c8f73d
child 32010 cb1a1c94b4cd
eliminated obsolete legacy_varify;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Jul 15 21:42:24 2009 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Jul 15 23:11:57 2009 +0200
     1.3 @@ -177,7 +177,6 @@
     1.4    let
     1.5      val b' = Morphism.binding phi b;
     1.6      val rhs' = Morphism.term phi rhs;
     1.7 -    val legacy_arg = (b', Term.close_schematic_term (Logic.legacy_varify rhs'));
     1.8      val arg = (b', Term.close_schematic_term rhs');
     1.9      val similar_body = Type.similar_types (rhs, rhs');
    1.10      (* FIXME workaround based on educated guess *)
    1.11 @@ -188,7 +187,7 @@
    1.12    in
    1.13      not (is_class andalso (similar_body orelse class_global)) ?
    1.14        (Context.mapping_result
    1.15 -        (Sign.add_abbrev PrintMode.internal tags legacy_arg)
    1.16 +        (Sign.add_abbrev PrintMode.internal tags arg)
    1.17          (ProofContext.add_abbrev PrintMode.internal tags arg)
    1.18        #-> (fn (lhs' as Const (d, _), _) =>
    1.19            similar_body ?