src/Pure/Isar/class.ML

--- a/src/Pure/Isar/class.ML	Sun Jun 08 23:30:50 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -333,12 +333,12 @@
     val rhs2 = Morphism.term phi2 rhs;
   in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
 
-fun const_declaration class phi0 prmode ((b, _), rhs) =
+fun target_const class phi0 prmode ((b, _), rhs) =
   let
     val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity;
     val guess_canonical = guess_morphism_identity (b, rhs) phi0;
   in
-    Generic_Target.locale_const_declaration class
+    Generic_Target.locale_target_const class
       (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs)
   end;
 
@@ -399,10 +399,10 @@
     val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
   in
     lthy
-    |> const_declaration class phi Syntax.mode_default ((b, mx), lhs)
+    |> target_const class phi Syntax.mode_default ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params
          ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
-    |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other)
+    |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
          Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class
   end;
@@ -413,10 +413,10 @@
     val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
   in
     lthy
-    |> const_declaration class phi prmode ((b, mx), lhs)
+    |> target_const class phi prmode ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
          ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
-    |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other)
+    |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
          prmode ((b, if null dangling_term_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class
   end;