# HG changeset patch
# User wenzelm
# Date 1333445301 -7200
# Node ID b79bf8288b298f06a61c38285d63007fa03206e5
# Parent  8f06d8ac46097ec8e601cd81391cf33b55ac1c9b
clarified generic_const vs. close_schematic_term;

diff -r 8f06d8ac4609 -r b79bf8288b29 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue Apr 03 11:21:17 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 11:28:21 2012 +0200
@@ -257,7 +257,7 @@
         |> 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)]))))
@@ -269,7 +269,7 @@
       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);
 
 
 
diff -r 8f06d8ac4609 -r b79bf8288b29 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Tue Apr 03 11:21:17 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 11:28:21 2012 +0200
@@ -61,8 +61,7 @@
           andalso List.last prefix' = (Class.class_prefix target, false)
         orelse same_shape);
     in
-      not is_canonical_class ?
-        Generic_Target.generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs')
+      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs')
     end) #>
   (fn lthy => lthy |> Generic_Target.const_declaration
     (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));