src/Pure/Isar/generic_target.ML

         context
         |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
         |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
     | NONE =>
         context
-        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
+        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t)
         |-> (fn (const as Const (c, _), _) => same_shape ?
               (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
                Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
   end;
 

   standard_declaration pred (fn phi =>
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
       val same_shape = Term.aconv_untyped (rhs, rhs');
-    in generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs') end);
+    in generic_const same_shape prmode ((b', mx), rhs') end);
 
 
 
 (** primitive theory operations **)