1.1 --- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 11:21:17 2012 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 11:28:21 2012 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4          |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
     1.5      | NONE =>
     1.6          context
     1.7 -        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
     1.8 +        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t)
     1.9          |-> (fn (const as Const (c, _), _) => same_shape ?
    1.10                (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
    1.11                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
    1.12 @@ -269,7 +269,7 @@
    1.13        val b' = Morphism.binding phi b;
    1.14        val rhs' = Morphism.term phi rhs;
    1.15        val same_shape = Term.aconv_untyped (rhs, rhs');
    1.16 -    in generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs') end);
    1.17 +    in generic_const same_shape prmode ((b', mx), rhs') end);
    1.18  
    1.19  
    1.20  

     2.1 --- a/src/Pure/Isar/named_target.ML	Tue Apr 03 11:21:17 2012 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 11:28:21 2012 +0200
     2.3 @@ -61,8 +61,7 @@
     2.4            andalso List.last prefix' = (Class.class_prefix target, false)
     2.5          orelse same_shape);
     2.6      in
     2.7 -      not is_canonical_class ?
     2.8 -        Generic_Target.generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs')
     2.9 +      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
    2.10      end) #>
    2.11    (fn lthy => lthy |> Generic_Target.const_declaration
    2.12      (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));