# HG changeset patch
# User wenzelm
# Date 1333438876 -7200
# Node ID d344f6d9cc85e7261a5c14b979e5fa4166a7ab0c
# Parent  57d486231c92b53cb60c104141e0318b591ac675
tuned;

diff -r 57d486231c92 -r d344f6d9cc85 src/Pure/Isar/generic_target.ML
--- 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);
 
 
 
diff -r 57d486231c92 -r d344f6d9cc85 src/Pure/Isar/named_target.ML
--- 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));