# 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);