tuned;

--- a/src/Pure/Isar/generic_target.ML	Mon Apr 02 23:55:25 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:41:16 2012 +0200
@@ -265,9 +265,8 @@
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
-      val rhs'' = Term.close_schematic_term rhs';
       val same_shape = Term.aconv_untyped (rhs, rhs');
-    in generic_const same_shape prmode ((b', mx), rhs'') end);
+    in generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs') end);
 
 
 

--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 23:55:25 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 09:41:16 2012 +0200
@@ -51,7 +51,6 @@
     let
       val b' = Morphism.binding phi b;
       val rhs' = Morphism.term phi rhs;
-      val rhs'' = Term.close_schematic_term rhs';
       val same_shape = Term.aconv_untyped (rhs, rhs');
 
       (* FIXME workaround based on educated guess *)
@@ -62,7 +61,8 @@
           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), rhs'')
+      not is_canonical_class ?
+        Generic_Target.generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs')
     end) #>
   (fn lthy => lthy |> Generic_Target.const_declaration
     (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));