1.1 --- a/src/Pure/Isar/generic_target.ML	Mon Apr 02 23:55:25 2012 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Tue Apr 03 09:41:16 2012 +0200
     1.3 @@ -265,9 +265,8 @@
     1.4      let
     1.5        val b' = Morphism.binding phi b;
     1.6        val rhs' = Morphism.term phi rhs;
     1.7 -      val rhs'' = Term.close_schematic_term rhs';
     1.8        val same_shape = Term.aconv_untyped (rhs, rhs');
     1.9 -    in generic_const same_shape prmode ((b', mx), rhs'') end);
    1.10 +    in generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs') end);
    1.11  
    1.12  
    1.13  

     2.1 --- a/src/Pure/Isar/named_target.ML	Mon Apr 02 23:55:25 2012 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Tue Apr 03 09:41:16 2012 +0200
     2.3 @@ -51,7 +51,6 @@
     2.4      let
     2.5        val b' = Morphism.binding phi b;
     2.6        val rhs' = Morphism.term phi rhs;
     2.7 -      val rhs'' = Term.close_schematic_term rhs';
     2.8        val same_shape = Term.aconv_untyped (rhs, rhs');
     2.9  
    2.10        (* FIXME workaround based on educated guess *)
    2.11 @@ -62,7 +61,8 @@
    2.12            andalso List.last prefix' = (Class.class_prefix target, false)
    2.13          orelse same_shape);
    2.14      in
    2.15 -      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs'')
    2.16 +      not is_canonical_class ?
    2.17 +        Generic_Target.generic_const same_shape prmode ((b', mx), Term.close_schematic_term rhs')
    2.18      end) #>
    2.19    (fn lthy => lthy |> Generic_Target.const_declaration
    2.20      (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));