# HG changeset patch
# User haftmann
# Date 1400773983 -7200
# Node ID 483b8c49a7bc1fa383b6e8764405b669d7f7df84
# Parent  9a631586e3e56b6720fd1174d4460796c3a3bd8c
tuned

diff -r 9a631586e3e5 -r 483b8c49a7bc src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 22 17:53:02 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 22 17:53:03 2014 +0200
@@ -275,21 +275,18 @@
                Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
   end;
 
+fun standard_const prmode ((b, mx), rhs) phi =
+  let
+    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), rhs') end;
+
 fun const pred prmode ((b, mx), rhs) =
-  standard_declaration pred (fn phi =>
-    let
-      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), rhs') end);
+  standard_declaration pred (standard_const prmode ((b, mx), rhs));
 
 fun locale_const locale prmode ((b, mx), rhs) =
-  locale_declaration locale true (fn phi =>
-    let
-      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), rhs') end)
+  locale_declaration locale true (standard_const prmode ((b, mx), rhs))
   #> const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);