# HG changeset patch # User haftmann # Date 1400773982 -7200 # Node ID 9a631586e3e56b6720fd1174d4460796c3a3bd8c # Parent 9c990475d44f2c4e53150ddfe45f2602ab1e9641 tuned names diff -r 9c990475d44f -r 9a631586e3e5 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu May 22 17:53:01 2014 +0200 +++ b/src/Pure/Isar/class.ML Thu May 22 17:53:02 2014 +0200 @@ -325,7 +325,7 @@ |> synchronize_class_syntax_target class end; -fun const_declaration class prmode (b, rhs) = +fun class_const class prmode (b, rhs) = Generic_Target.locale_declaration class true (fn phi => let val b' = Morphism.binding phi b; @@ -342,10 +342,9 @@ in not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', NoSyn), rhs') end) #> - Generic_Target.const_declaration - (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs); + Generic_Target.const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, NoSyn), rhs); -fun class_const (type_params, term_params) class phi ((b, mx), rhs) thy = +fun global_const (type_params, term_params) class phi ((b, mx), rhs) thy = let val class_params = map fst (these_params thy [class]); val additional_params = @@ -370,7 +369,7 @@ |> Sign.add_const_constraint (c', SOME ty') end; -fun class_abbrev prmode class phi ((b, mx), rhs) thy = +fun global_abbrev prmode class phi ((b, mx), rhs) thy = let val unchecks = these_unchecks thy [class]; val b' = Morphism.binding phi b; @@ -389,12 +388,12 @@ in fun const class ((b, mx), lhs) params = - const_declaration class Syntax.mode_default (b, lhs) - #> target_extension (class_const params) class ((b, mx), lhs); + class_const class Syntax.mode_default (b, lhs) + #> target_extension (global_const params) class ((b, mx), lhs); fun abbrev class prmode ((b, mx), lhs) t' = - const_declaration class prmode (b, lhs) - #> target_extension (class_abbrev prmode) class ((b, mx), t'); + class_const class prmode (b, lhs) + #> target_extension (global_abbrev prmode) class ((b, mx), t'); end; diff -r 9c990475d44f -r 9a631586e3e5 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu May 22 17:53:01 2014 +0200 +++ b/src/Pure/Isar/generic_target.ML Thu May 22 17:53:02 2014 +0200 @@ -29,9 +29,9 @@ val standard_declaration: (int * int -> bool) -> declaration -> local_theory -> local_theory val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> Context.generic -> Context.generic - val const_declaration: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> + val const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory - val locale_const_declaration: string -> Syntax.mode -> (binding * mixfix) * term -> + val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory @@ -275,7 +275,7 @@ Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) end; -fun const_declaration pred prmode ((b, mx), rhs) = +fun const pred prmode ((b, mx), rhs) = standard_declaration pred (fn phi => let val b' = Morphism.binding phi b; @@ -283,15 +283,14 @@ val same_shape = Term.aconv_untyped (rhs, rhs'); in generic_const same_shape prmode ((b', mx), rhs') end); -fun locale_const_declaration locale 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) - #> const_declaration - (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); + #> const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); (* registrations and dependencies *) @@ -324,8 +323,7 @@ fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) - #-> (fn (lhs, def) => - const_declaration (op <>) Syntax.mode_default ((b, mx), lhs) + #-> (fn (lhs, def) => const (op <>) Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun theory_notes kind global_facts local_facts = @@ -341,8 +339,7 @@ (Sign.add_abbrev (#1 prmode) (b, t) #-> (fn (lhs, _) => (* FIXME type_params!? *) Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs)) - #-> (fn lhs => - const_declaration (op <>) prmode + #-> (fn lhs => const (op <>) prmode ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs))); fun theory_declaration decl = diff -r 9c990475d44f -r 9a631586e3e5 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Thu May 22 17:53:01 2014 +0200 +++ b/src/Pure/Isar/named_target.ML Thu May 22 17:53:02 2014 +0200 @@ -50,14 +50,14 @@ (* define *) -fun locale_foundation target (((b, U), mx), (b_def, rhs)) params = +fun locale_foundation locale (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params - #-> (fn (lhs, def) => Generic_Target.locale_const_declaration target Syntax.mode_default ((b, mx), lhs) + #-> (fn (lhs, def) => Generic_Target.locale_const locale Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); -fun class_foundation target (((b, U), mx), (b_def, rhs)) params = +fun class_foundation class (((b, U), mx), (b_def, rhs)) params = Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params - #-> (fn (lhs, def) => Class.const target ((b, mx), lhs) params + #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params #> pair (lhs, def)); fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = @@ -75,13 +75,13 @@ (* abbrev *) -fun locale_abbrev target prmode (b, mx) (t, _) xs = +fun locale_abbrev locale prmode (b, mx) (t, _) xs = Generic_Target.background_abbrev (b, t) xs - #-> (fn (lhs, _) => Generic_Target.locale_const_declaration target prmode ((b, mx), lhs)); + #-> (fn (lhs, _) => Generic_Target.locale_const locale prmode ((b, mx), lhs)); -fun class_abbrev target prmode (b, mx) (t, t') xs = +fun class_abbrev class prmode (b, mx) (t, t') xs = Generic_Target.background_abbrev (b, t) xs - #-> (fn (lhs, _) => Class.abbrev target prmode ((b, mx), lhs) t'); + #-> (fn (lhs, _) => Class.abbrev class prmode ((b, mx), lhs) t'); fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) = if is_class then class_abbrev target