--- 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;
--- 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 =
--- 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